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

proof

let x be Element of (product <*G1,G2*>); :: thesis: ex y being Element of (product <*H1,H2*>) st S₁[x,y]
consider a being Element of G1, h being Element of G2 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 G2 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 (product <*G1,G2*>) 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 (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st
( x = <*x1,x2*> & b₁ . x = <*(f . x1),(g . x2)*> ) ; :: thesis: verum