defpred S₁[ object , object ] means for h being Function st h = $1 holds
$2 = [(f . (pr1 h)),(g . (pr2 h))];
set Y = [|A,B|] . rj;
set X = ([|A,B|] #) . pj;
A1: ([|A,B|] #) . pj = product ([|A,B|] * pj) by FINSEQ_2:def 5;
A2: for x being object st x in ([|A,B|] #) . pj holds
ex y being object st
( y in [|A,B|] . rj & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in ([|A,B|] #) . pj implies ex y being object st
( y in [|A,B|] . rj & S₁[x,y] ) )
A3: rng pj c= I by FINSEQ_1:def 4;
assume x in ([|A,B|] #) . pj ; :: thesis: ex y being object st
( y in [|A,B|] . rj & S₁[x,y] )
then consider h1 being Function such that
A4: h1 = x and
A5: dom h1 = dom ([|A,B|] * pj) and
A6: for z being object st z in dom ([|A,B|] * pj) holds
h1 . z in ([|A,B|] * pj) . z by A1, CARD_3:def 5;
A7: dom [|A,B|] = I by PARTFUN1:def 2;
then A8: dom h1 = dom pj by A5, A3, RELAT_1:27;
then A9: dom (pr1 h1) = dom pj by MCART_1:def 12;
dom A = I by PARTFUN1:def 2;
then A10: dom (pr1 h1) = dom (A * pj) by A3, A9, RELAT_1:27;
for z being object st z in dom (A * pj) holds
(pr1 h1) . z in (A * pj) . z

proof

let z be object ; :: thesis: ( z in dom (A * pj) implies (pr1 h1) . z in (A * pj) . z )
assume A11: z in dom (A * pj) ; :: thesis: (pr1 h1) . z in (A * pj) . z
dom ([|A,B|] * pj) = dom pj by A7, A3, RELAT_1:27;
then A12: ([|A,B|] * pj) . z = [|A,B|] . (pj . z) by A9, A10, A11, FUNCT_1:12;
( h1 . z in ([|A,B|] * pj) . z & pj . z in rng pj ) by A5, A6, A8, A9, A10, A11, FUNCT_1:def 3;
then h1 . z in [:(A . (pj . z)),(B . (pj . z)):] by A3, A12, PBOOLE:def 16;
then consider a, b being object such that
A13: a in A . (pj . z) and
b in B . (pj . z) and
A14: h1 . z = [a,b] by ZFMISC_1:def 2;
(pr1 h1) . z = (h1 . z) `1 by A8, A9, A10, A11, MCART_1:def 12
.= a by A14 ;
hence (pr1 h1) . z in (A * pj) . z by A11, A13, FUNCT_1:12; :: thesis: verum

end;

then pr1 h1 in product (A * pj) by A10, CARD_3:9;
then pr1 h1 in (A #) . pj by FINSEQ_2:def 5;
then pr1 h1 in dom f by FUNCT_2:def 1;
then A15: f . (pr1 h1) in rng f by FUNCT_1:3;
take y = [(f . (pr1 h1)),(g . (pr2 h1))]; :: thesis: ( y in [|A,B|] . rj & S₁[x,y] )
( rng f c= A . rj & rng g c= B . rj ) by RELAT_1:def 19;
then A16: [:(rng f),(rng g):] c= [:(A . rj),(B . rj):] by ZFMISC_1:96;
A17: dom (pr2 h1) = dom pj by A8, MCART_1:def 13;
A18: dom B = I by PARTFUN1:def 2;
then A19: dom (pr2 h1) = dom (B * pj) by A3, A17, RELAT_1:27;
A20: for z being object st z in dom (B * pj) holds
(pr2 h1) . z in (B * pj) . z

proof

let z be object ; :: thesis: ( z in dom (B * pj) implies (pr2 h1) . z in (B * pj) . z )
assume A21: z in dom (B * pj) ; :: thesis: (pr2 h1) . z in (B * pj) . z
dom ([|A,B|] * pj) = dom pj by A7, A3, RELAT_1:27;
then A22: ([|A,B|] * pj) . z = [|A,B|] . (pj . z) by A17, A19, A21, FUNCT_1:12;
( h1 . z in ([|A,B|] * pj) . z & pj . z in rng pj ) by A5, A6, A8, A17, A19, A21, FUNCT_1:def 3;
then h1 . z in [:(A . (pj . z)),(B . (pj . z)):] by A3, A22, PBOOLE:def 16;
then consider a, b being object such that
a in A . (pj . z) and
A23: b in B . (pj . z) and
A24: h1 . z = [a,b] by ZFMISC_1:def 2;
(pr2 h1) . z = (h1 . z) `2 by A8, A17, A19, A21, MCART_1:def 13
.= b by A24 ;
hence (pr2 h1) . z in (B * pj) . z by A21, A23, FUNCT_1:12; :: thesis: verum

end;

dom (pr2 h1) = dom pj by A8, MCART_1:def 13;
then dom (pr2 h1) = dom (B * pj) by A18, A3, RELAT_1:27;
then pr2 h1 in product (B * pj) by A20, CARD_3:9;
then pr2 h1 in (B #) . pj by FINSEQ_2:def 5;
then pr2 h1 in dom g by FUNCT_2:def 1;
then g . (pr2 h1) in rng g by FUNCT_1:3;
then [(f . (pr1 h1)),(g . (pr2 h1))] in [:(rng f),(rng g):] by A15, ZFMISC_1:87;
then [(f . (pr1 h1)),(g . (pr2 h1))] in [:(A . rj),(B . rj):] by A16;
hence y in [|A,B|] . rj by PBOOLE:def 16; :: thesis: S₁[x,y]
let h be Function; :: thesis: ( h = x implies y = [(f . (pr1 h)),(g . (pr2 h))] )
assume x = h ; :: thesis: y = [(f . (pr1 h)),(g . (pr2 h))]
hence y = [(f . (pr1 h)),(g . (pr2 h))] by A4; :: thesis: verum

end;

consider F being Function of (([|A,B|] #) . pj),([|A,B|] . rj) such that
A25: for x being object st x in ([|A,B|] #) . pj holds
S₁[x,F . x] from FUNCT_2:sch 1(A2);
take F ; :: thesis: for h being Function st h in ([|A,B|] #) . pj holds
F . h = [(f . (pr1 h)),(g . (pr2 h))]
thus for h being Function st h in ([|A,B|] #) . pj holds
F . h = [(f . (pr1 h)),(g . (pr2 h))] by A25; :: thesis: verum