deffunc H₁( set ) -> set = H . $1;
deffunc H₂( set ) -> Variable = y;
set A = dom H;
defpred S₁[ set ] means H . $1 = x;
thus ex f being Function st
( dom f = dom H & ( for a being set st a in dom H holds
( ( S₁[a] implies f . a = H₂(a) ) & ( not S₁[a] implies f . a = H₁(a) ) ) ) ) from PARTFUN1:sch 1(); :: thesis: verum