set xy = <*x,y*>;

set G = <*G1,G2*>;

A1: dom (Carrier <*G1,G2*>) = {1,2} by PARTFUN1:def 2;

A2: <*x,y*> . 2 = y by FINSEQ_1:44;

A3: <*G1,G2*> . 2 = G2 by FINSEQ_1:44;

A4: <*G1,G2*> . 1 = G1 by FINSEQ_1:44;

A5: <*x,y*> . 1 = x by FINSEQ_1:44;

A6: for a being object st a in {1,2} holds

<*x,y*> . a in (Carrier <*G1,G2*>) . a

then <*x,y*> in product (Carrier <*G1,G2*>) by A1, A6, CARD_3:9;

hence <*x,y*> is Element of (product <*G1,G2*>) by Def2; :: thesis: verum

set G = <*G1,G2*>;

A1: dom (Carrier <*G1,G2*>) = {1,2} by PARTFUN1:def 2;

A2: <*x,y*> . 2 = y by FINSEQ_1:44;

A3: <*G1,G2*> . 2 = G2 by FINSEQ_1:44;

A4: <*G1,G2*> . 1 = G1 by FINSEQ_1:44;

A5: <*x,y*> . 1 = x by FINSEQ_1:44;

A6: for a being object st a in {1,2} holds

<*x,y*> . a in (Carrier <*G1,G2*>) . a

proof

dom <*x,y*> = {1,2}
by FINSEQ_1:2, FINSEQ_1:89;
let a be object ; :: 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

end;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;

end;

then <*x,y*> in product (Carrier <*G1,G2*>) by A1, A6, CARD_3:9;

hence <*x,y*> is Element of (product <*G1,G2*>) by Def2; :: thesis: verum