defpred S₁[ Element of product F, Element of product G] means for i being object st i in dom h holds
ex hi being Function of (F . i),(G . i) st
( hi = h . i & $2 . i = hi . ($1 . i) );
A2: for x being Element of product F ex y being Element of product G st S₁[x,y]

proof

let x be Element of product F; :: thesis: ex y being Element of product G st S₁[x,y]
defpred S₂[ object , object ] means ex hi being Function of (F . $1),(G . $1) st
( hi = h . $1 & $2 = hi . (x . $1) );
A3: for i being object st i in dom h holds
ex y being object st S₂[i,y]

proof

let i be object ; :: thesis: ( i in dom h implies ex y being object st S₂[i,y] )
assume i in dom h ; :: thesis: ex y being object st S₂[i,y]
then reconsider hi = h . i as Function of (F . i),(G . i) by A1;
take hi . (x . i) ; :: thesis: S₂[i,hi . (x . i)]
thus S₂[i,hi . (x . i)] ; :: thesis: verum

end;

consider y being Function such that
A4: ( dom y = dom h & ( for i being object st i in dom h holds
S₂[i,y . i] ) ) from CLASSES1:sch 1(A3);

now :: thesis: for i being object st i in dom G holds
y . i in G . i

let i be object ; :: thesis: ( i in dom G implies y . i in G . i )
assume A5: i in dom G ; :: thesis: y . i in G . i
then consider hi being Function of (F . i),(G . i) such that
A7: ( hi = h . i & y . i = hi . (x . i) ) by A1, A4;
thus y . i in G . i by A1, A5, A7, CARD_3:9, FUNCT_2:5; :: thesis: verum

end;

then reconsider y = y as Element of product G by A1, A4, CARD_3:9;
take y ; :: thesis: S₁[x,y]
let i be object ; :: thesis: ( i in dom h implies ex hi being Function of (F . i),(G . i) st
( hi = h . i & y . i = hi . (x . i) ) )
assume i in dom h ; :: thesis: ex hi being Function of (F . i),(G . i) st
( hi = h . i & y . i = hi . (x . i) )
hence ex hi being Function of (F . i),(G . i) st
( hi = h . i & y . i = hi . (x . i) ) by A4; :: thesis: verum

end;

thus ex p being Function of (product F),(product G) st
for x being Element of product F holds S₁[x,p . x] from FUNCT_2:sch 3(A2); :: thesis: verum