set xy = <*x,y*>;
set G = <*G1,G2*>;
A1: dom (Carrier <*G1,G2*>) = {1,2} by PARTFUN1:def 4;
A2: <*x,y*> . 2 = y by FINSEQ_1:61;
A3: <*G1,G2*> . 2 = G2 by FINSEQ_1:61;
A4: <*G1,G2*> . 1 = G1 by FINSEQ_1:61;
A5: <*x,y*> . 1 = x by FINSEQ_1:61;
A6: for a being set st a in {1,2} holds
<*x,y*> . a in (Carrier <*G1,G2*>) . a

proof

let a be set ; :: thesis: ( a in {1,2} implies <*x,y*> . a in (Carrier <*G1,G2*>) . a )
assume A7: a in {1,2} ; :: thesis: <*x,y*> . a in (Carrier <*G1,G2*>) . a

per cases ( a = 1 or a = 2 ) by A7, TARSKI:def 2;

suppose A8: a = 1 ; :: thesis: <*x,y*> . a in (Carrier <*G1,G2*>) . a

then ex R being 1-sorted st
( R = <*G1,G2*> . 1 & (Carrier <*G1,G2*>) . 1 = the carrier of R ) by A7, PRALG_1:def 13;
hence <*x,y*> . a in (Carrier <*G1,G2*>) . a by A5, A4, A8; :: thesis: verum

end;

suppose A9: a = 2 ; :: thesis: <*x,y*> . a in (Carrier <*G1,G2*>) . a

then ex R being 1-sorted st
( R = <*G1,G2*> . 2 & (Carrier <*G1,G2*>) . 2 = the carrier of R ) by A7, PRALG_1:def 13;
hence <*x,y*> . a in (Carrier <*G1,G2*>) . a by A2, A3, A9; :: thesis: verum

end;

end;

end;

dom <*x,y*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
then <*x,y*> in product (Carrier <*G1,G2*>) by A1, A6, CARD_3:18;
hence <*x,y*> is Element of (product <*G1,G2*>) by Def2; :: thesis: verum