set xy = <*x*>;
set G = <*G1*>;
A1: dom (Carrier <*G1*>) = {1} by PARTFUN1:def 2;
A4: for a being object st a in {1} holds
<*x*> . a in (Carrier <*G1*>) . a

proof

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

end;

dom <*x*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;
then <*x*> in product (Carrier <*G1*>) by A1, A4, CARD_3:9;
hence <*x*> is Element of (product <*G1*>) by Def2; :: thesis: verum