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

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

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

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

hence ex b