defpred S1[ 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 S1[x,y]
proof
let x be
Element of
product F;
ex y being Element of product G st S1[x,y]
defpred S2[
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
S2[
i,
y]
proof
let i be
object ;
( i in dom h implies ex y being object st S2[i,y] )
assume
i in dom h
;
ex y being object st S2[i,y]
then reconsider hi =
h . i as
Function of
(F . i),
(G . i) by A1;
take
hi . (x . i)
;
S2[i,hi . (x . i)]
thus
S2[
i,
hi . (x . i)]
;
verum
end;
consider y being
Function such that A4:
(
dom y = dom h & ( for
i being
object st
i in dom h holds
S2[
i,
y . i] ) )
from CLASSES1:sch 1(A3);
then reconsider y =
y as
Element of
product G by A1, A4, CARD_3:9;
take
y
;
S1[x,y]
let i be
object ;
( 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
;
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;
verum
end;
thus
ex p being Function of (product F),(product G) st
for x being Element of product F holds S1[x,p . x]
from FUNCT_2:sch 3(A2); verum