defpred S1[ 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 S1[x,y]
proof
let x be
Element of
(product <*G1,G2*>);
ex y being Element of (product <*H1,H2*>) st S1[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)*>
;
S1[x,<*(f . a),(g . h)*>]
take
a
;
ex x2 being Element of G2 st
( x = <*a,x2*> & <*(f . a),(g . h)*> = <*(f . a),(g . x2)*> )
take
h
;
( 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;
verum
end;
ex h being Function of (product <*G1,G2*>),(product <*H1,H2*>) st
for x being Element of (product <*G1,G2*>) holds S1[x,h . x]
from FUNCT_2:sch 3(A1);
hence
ex b1 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*> & b1 . x = <*(f . x1),(g . x2)*> )
; verum