let G, H be non empty multMagma ; :: thesis: for x being Element of (product <*G,H*>) ex g being Element of G ex h being Element of H st x = <*g,h*>
let x be Element of (product <*G,H*>); :: thesis: ex g being Element of G ex h being Element of H st x = <*g,h*>
the carrier of (product <*G,H*>) = product (Carrier <*G,H*>) by GROUP_7:def 2;
then consider g being Function such that
A1: x = g and
A2: dom g = dom (Carrier <*G,H*>) and
A3: for y being set st y in dom (Carrier <*G,H*>) holds
g . y in (Carrier <*G,H*>) . y by CARD_3:def 5;
A4: dom (Carrier <*G,H*>) = {1,2} by PARTFUN1:def 4;
then reconsider g = g as FinSequence by A2, FINSEQ_1:4, FINSEQ_1:def 2;
A5: g . 1 in (Carrier <*G,H*>) . 1 by A3, A4, Lm1;
ex R being 1-sorted st
( R = <*G,H*> . 1 & (Carrier <*G,H*>) . 1 = the carrier of R ) by Lm1, PRALG_1:def 13;
then reconsider g1 = g . 1 as Element of G by A5, FINSEQ_1:61;
A6: g . 2 in (Carrier <*G,H*>) . 2 by A3, A4, Lm2;
ex R being 1-sorted st
( R = <*G,H*> . 2 & (Carrier <*G,H*>) . 2 = the carrier of R ) by Lm2, PRALG_1:def 13;
then reconsider h1 = g . 2 as Element of H by A6, FINSEQ_1:61;
take g1 ; :: thesis: ex h being Element of H st x = <*g1,h*>
take h1 ; :: thesis: x = <*g1,h1*>
len g = 2 by A2, A4, FINSEQ_1:4, FINSEQ_1:def 3;
hence x = <*g1,h1*> by A1, FINSEQ_1:61; :: thesis: verum