let G1, G2 be Group; :: thesis: for x being Element of product (Carrier <*G1,G2*>) holds
( x . 1 in G1 & x . 2 in G2 & dom x = {1,2} )
let x be Element of product (Carrier <*G1,G2*>); :: thesis: ( x . 1 in G1 & x . 2 in G2 & dom x = {1,2} )
x is Element of the carrier of (product <*G1,G2*>) by GROUP_7:def 2;
hence ( x . 1 in G1 & x . 2 in G2 & dom x = {1,2} ) by Th6; :: thesis: verum