let G1, G2 be Group; :: thesis: for H1 being Subgroup of G1
for H2 being Subgroup of G2
for h1 being Element of G1 st h1 in H1 holds
for h2 being Element of G2 st h2 in H2 holds
<*h1,h2*> in product <*H1,H2*>
let H1 be Subgroup of G1; :: thesis: for H2 being Subgroup of G2
for h1 being Element of G1 st h1 in H1 holds
for h2 being Element of G2 st h2 in H2 holds
<*h1,h2*> in product <*H1,H2*>
let H2 be Subgroup of G2; :: thesis: for h1 being Element of G1 st h1 in H1 holds
for h2 being Element of G2 st h2 in H2 holds
<*h1,h2*> in product <*H1,H2*>
let h1 be Element of G1; :: thesis: ( h1 in H1 implies for h2 being Element of G2 st h2 in H2 holds
<*h1,h2*> in product <*H1,H2*> )
assume A1: h1 in H1 ; :: thesis: for h2 being Element of G2 st h2 in H2 holds
<*h1,h2*> in product <*H1,H2*>
let h2 be Element of G2; :: thesis: ( h2 in H2 implies <*h1,h2*> in product <*H1,H2*> )
assume A2: h2 in H2 ; :: thesis: <*h1,h2*> in product <*H1,H2*>
set H = <*H1,H2*>;
A3: dom (Carrier <*H1,H2*>) = {1,2} by PARTFUN1:def 2;
A4: for a being object st a in {1,2} holds
<*h1,h2*> . a in (Carrier <*H1,H2*>) . a

proof

let a be object ; :: thesis: ( a in {1,2} implies <*h1,h2*> . a in (Carrier <*H1,H2*>) . a )
assume B1: a in {1,2} ; :: thesis: <*h1,h2*> . a in (Carrier <*H1,H2*>) . a

per cases then ( a = 1 or a = 2 ) by TARSKI:def 2;

suppose B2: a = 1 ; :: thesis: <*h1,h2*> . a in (Carrier <*H1,H2*>) . a

then ex R being 1-sorted st
( R = <*H1,H2*> . 1 & (Carrier <*H1,H2*>) . 1 = the carrier of R ) by B1, PRALG_1:def 15;
hence <*h1,h2*> . a in (Carrier <*H1,H2*>) . a by A1, B2; :: thesis: verum

end;

suppose B4: a = 2 ; :: thesis: <*h1,h2*> . a in (Carrier <*H1,H2*>) . a

then ex R being 1-sorted st
( R = <*H1,H2*> . 2 & (Carrier <*H1,H2*>) . 2 = the carrier of R ) by B1, PRALG_1:def 15;
hence <*h1,h2*> . a in (Carrier <*H1,H2*>) . a by A2, B4; :: thesis: verum

end;

end;

end;

dom <*h1,h2*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
then <*h1,h2*> in product (Carrier <*H1,H2*>) by A3, A4, CARD_3:9;
hence <*h1,h2*> in product <*H1,H2*> by GROUP_7:def 2; :: thesis: verum