consider e being Function of (SetVal V,(p => q)),(SetVal V,(p => r));
e is Function-yielding ;
hence ex b₁ being Function of (SetVal V,(p => q)),(SetVal V,(p => r)) st b₁ is Function-yielding ; :: thesis: verum