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₁ being Function of (SetVal (V,(p => q))),(SetVal (V,(p => r))) st b₁ is Function-yielding ; :: thesis: verum