defpred S₁[ set , set ] means ex x1 being Element of ex x2 being Element of st
( $1 = <*x1,x2*> & $2 = <*(f . x1),(g . x2)*> );
A1: for x being Element of ex y being Element of st S₁[x,y]

proof

let x be Element of ; :: thesis: ex y being Element of st S₁[x,y]
consider a being Element of , h being Element of such that
A2: x = <*a,h*> by Th1;
take <*(f . a),(g . h)*> ; :: thesis: S₁[x,<*(f . a),(g . h)*>]
take a ; :: thesis: ex x2 being Element of st
( x = <*a,x2*> & <*(f . a),(g . h)*> = <*(f . a),(g . x2)*> )
take h ; :: thesis: ( x = <*a,h*> & <*(f . a),(g . h)*> = <*(f . a),(g . h)*> )
thus ( x = <*a,h*> & <*(f . a),(g . h)*> = <*(f . a),(g . h)*> ) by A2; :: thesis: verum

end;

ex h being Function of (product <*G1,G2*>),(product <*H1,H2*>) st
for x being Element of holds S₁[x,h . x] from FUNCT_2:sch 3(A1);
hence ex b₁ being Function of (product <*G1,G2*>),(product <*H1,H2*>) st
for x being Element of ex x1 being Element of ex x2 being Element of st
( x = <*x1,x2*> & b₁ . x = <*(f . x1),(g . x2)*> ) ; :: thesis: verum