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