let A, G be Group; :: thesis: for a being Element of A
for g being Element of G holds <*a,g*> in product (Carrier <*A,G*>)
let a be Element of A; :: thesis: for g being Element of G holds <*a,g*> in product (Carrier <*A,G*>)
let g be Element of G; :: thesis: <*a,g*> in product (Carrier <*A,G*>)
<*a,g*> in the carrier of (product <*A,G*>) ;
hence <*a,g*> in product (Carrier <*A,G*>) by GROUP_7:def 2; :: thesis: verum