set e = the Element of SetVal (V,(p => (q => r)));

the Element of SetVal (V,(p => (q => r))) is Function-yielding ;

hence ex b_{1} being Element of SetVal (V,(p => (q => r))) st b_{1} is Function-yielding
; :: thesis: verum

the Element of SetVal (V,(p => (q => r))) is Function-yielding ;

hence ex b