let G1, G2 be Group; :: thesis: for x being Element of (product <*G1,G2*>) holds
( x . 1 in G1 & x . 2 in G2 & dom x = {1,2} )
let x be Element of (product <*G1,G2*>); :: thesis: ( x . 1 in G1 & x . 2 in G2 & dom x = {1,2} )
A1: dom (Carrier <*G1,G2*>) = {1,2} by PARTFUN1:def 2;
x in the carrier of (product <*G1,G2*>) ;
then x in product (Carrier <*G1,G2*>) by GROUP_7:def 2;
then consider f being Function such that
A2: ( x = f & dom f = dom (Carrier <*G1,G2*>) & ( for y being object st y in dom (Carrier <*G1,G2*>) holds
f . y in (Carrier <*G1,G2*>) . y ) ) by CARD_3:def 5;
thus x . 1 in G1 :: thesis: ( x . 2 in G2 & dom x = {1,2} )

proof

B2: 1 in dom (Carrier <*G1,G2*>) by A1, TARSKI:def 2;
then ex R being 1-sorted st
( R = <*G1,G2*> . 1 & (Carrier <*G1,G2*>) . 1 = the carrier of R ) by PRALG_1:def 15;
hence x . 1 in G1 by A2, B2; :: thesis: verum

end;

thus x . 2 in G2 :: thesis: dom x = {1,2}

proof

B2: 2 in dom (Carrier <*G1,G2*>) by A1, TARSKI:def 2;
then ex R being 1-sorted st
( R = <*G1,G2*> . 2 & (Carrier <*G1,G2*>) . 2 = the carrier of R ) by PRALG_1:def 15;
hence x . 2 in G2 by A2, B2; :: thesis: verum

end;

thus dom x = {1,2} by A2, PARTFUN1:def 2; :: thesis: verum