set xy = <*x*>;

set G = <*G1*>;

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

A2: <*G1*> . 1 = G1 by FINSEQ_1:def 8;

A3: <*x*> . 1 = x by FINSEQ_1:def 8;

A4: for a being object st a in {1} holds

<*x*> . a in (Carrier <*G1*>) . a

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

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

set G = <*G1*>;

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

A2: <*G1*> . 1 = G1 by FINSEQ_1:def 8;

A3: <*x*> . 1 = x by FINSEQ_1:def 8;

A4: for a being object st a in {1} holds

<*x*> . a in (Carrier <*G1*>) . a

proof

dom <*x*> = {1}
by FINSEQ_1:2, FINSEQ_1:def 8;
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 13;

hence <*x*> . a in (Carrier <*G1*>) . a by A3, A2, A6; :: thesis: verum

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

hence <*x*> . a in (Carrier <*G1*>) . a by A3, A2, A6; :: thesis: verum

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

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