set xy = <*x*>;
set G = <*G1*>;
A1: dom <*x*> = {1} by FINSEQ_1:4, FINSEQ_1:def 8;
A2: dom (Carrier <*G1*>) = {1} by PARTFUN1:def 4;
A3: ( <*x*> . 1 = x & <*G1*> . 1 = G1 ) by FINSEQ_1:def 8;
for a being set st a in {1} holds
<*x*> . a in (Carrier <*G1*>) . a

proof

let a be set ; :: thesis: ( a in {1} implies <*x*> . a in (Carrier <*G1*>) . a )
assume A4: a in {1} ; :: thesis: <*x*> . a in (Carrier <*G1*>) . a
then A5: a = 1 by TARSKI:def 1;
then ex R being 1-sorted st
( R = <*G1*> . 1 & (Carrier <*G1*>) . 1 = the carrier of R ) by A4, PRALG_1:def 13;
hence <*x*> . a in (Carrier <*G1*>) . a by A3, A5; :: thesis: verum

end;

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