set xy = <*x,y,z*>;

set G = <*G1,G2,G3*>;

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

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

A3: <*G1,G2,G3*> . 1 = G1 by FINSEQ_1:45;

A4: <*x,y,z*> . 3 = z by FINSEQ_1:45;

A5: <*G1,G2,G3*> . 3 = G3 by FINSEQ_1:45;

A6: <*G1,G2,G3*> . 2 = G2 by FINSEQ_1:45;

A7: <*x,y,z*> . 1 = x by FINSEQ_1:45;

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

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

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

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

set G = <*G1,G2,G3*>;

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

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

A3: <*G1,G2,G3*> . 1 = G1 by FINSEQ_1:45;

A4: <*x,y,z*> . 3 = z by FINSEQ_1:45;

A5: <*G1,G2,G3*> . 3 = G3 by FINSEQ_1:45;

A6: <*G1,G2,G3*> . 2 = G2 by FINSEQ_1:45;

A7: <*x,y,z*> . 1 = x by FINSEQ_1:45;

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

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

proof

dom <*x,y,z*> = {1,2,3}
by FINSEQ_1:89, FINSEQ_3:1;
let a be object ; :: thesis: ( a in {1,2,3} implies <*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a )

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

end;assume A9: 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 A9, ENUMSET1:def 1;

end;

suppose A10:
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 A9, PRALG_1:def 13;

hence <*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a by A7, A3, A10; :: thesis: verum

end;( R = <*G1,G2,G3*> . 1 & (Carrier <*G1,G2,G3*>) . 1 = the carrier of R ) by A9, PRALG_1:def 13;

hence <*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a by A7, A3, A10; :: thesis: verum

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

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