set xy = <*x,y,z*>;
set G = <*G1,G2,G3*>;
A1: dom <*x,y,z*> = {1,2,3} by FINSEQ_3:1, FINSEQ_3:30;
A2: dom (Carrier <*G1,G2,G3*>) = {1,2,3} by PARTFUN1:def 4;
A3: ( <*x,y,z*> . 1 = x & <*x,y,z*> . 2 = y & <*x,y,z*> . 3 = z & <*G1,G2,G3*> . 1 = G1 & <*G1,G2,G3*> . 2 = G2 & <*G1,G2,G3*> . 3 = G3 ) by FINSEQ_1:62;
for a being set st a in {1,2,3} holds
<*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a

proof

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

per cases ( a = 1 or a = 2 or a = 3 ) by A4, ENUMSET1:def 1;

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

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

end;

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

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

end;

suppose A7: a = 3 ; :: thesis: <*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a

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

end;

end;

end;

then <*x,y,z*> in product (Carrier <*G1,G2,G3*>) by A1, A2, CARD_3:18;
hence <*x,y,z*> is Element of (product <*G1,G2,G3*>) by Def2; :: thesis: verum