let G be Group; :: thesis: for H, K being Subgroup of G ex phi being Function of (product (Carrier <*H,K*>)),G st
( ( for h, k being Element of G st h in H & k in K holds
phi . <*h,k*> = h * k ) & ( phi is one-to-one implies H /\ K = (1). G ) & ( H /\ K = (1). G implies phi is one-to-one ) )
let H, K be Subgroup of G; :: thesis: ex phi being Function of (product (Carrier <*H,K*>)),G st
( ( for h, k being Element of G st h in H & k in K holds
phi . <*h,k*> = h * k ) & ( phi is one-to-one implies H /\ K = (1). G ) & ( H /\ K = (1). G implies phi is one-to-one ) )
defpred S₁[ Element of product (Carrier <*H,K*>), Element of G] means ex h, k being Element of G st
( h in H & k in K & $1 = <*h,k*> & $2 = h * k );
A1: for x being Element of product (Carrier <*H,K*>) ex y being Element of G st S₁[x,y]

proof

let x be Element of product (Carrier <*H,K*>); :: thesis: ex y being Element of G st S₁[x,y]
x in product (Carrier <*H,K*>) ;
then x in the carrier of (product <*H,K*>) by GROUP_7:def 2;
then B1: ( x . 1 in H & x . 2 in K & dom x = {1,2} ) by Th6;
then ( x . 1 in H & x . 1 in G & x . 2 in K & x . 2 in G ) by GROUP_2:40;
then consider h, k being Element of G such that
B2: ( h = x . 1 & k = x . 2 & h in H & k in K ) ;
len x = 2 by B1, FINSEQ_1:2, FINSEQ_1:def 3;
then B3: x = <*h,k*> by B2, FINSEQ_1:44;
take y = h * k; :: thesis: S₁[x,y]
thus S₁[x,y] by B2, B3; :: thesis: verum

end;

consider phi being Function of (product (Carrier <*H,K*>)),G such that
A2: for x being Element of product (Carrier <*H,K*>) holds S₁[x,phi . x] from FUNCT_2:sch 3(A1);
take phi ; :: thesis: ( ( for h, k being Element of G st h in H & k in K holds
phi . <*h,k*> = h * k ) & ( phi is one-to-one implies H /\ K = (1). G ) & ( H /\ K = (1). G implies phi is one-to-one ) )
A3: for h, k being Element of G st h in H & k in K holds
phi . <*h,k*> = h * k

proof

let h, k be Element of G; :: thesis: ( h in H & k in K implies phi . <*h,k*> = h * k )
assume B1: h in H ; :: thesis: ( not k in K or phi . <*h,k*> = h * k )
assume k in K ; :: thesis: phi . <*h,k*> = h * k
then <*h,k*> in product <*H,K*> by B1, Th7;
then reconsider x = <*h,k*> as Element of product (Carrier <*H,K*>) by GROUP_7:def 2;
consider h1, k1 being Element of G such that
B3: ( h1 in H & k1 in K & x = <*h1,k1*> & phi . x = h1 * k1 ) by A2;
( h1 = h & k1 = k ) by B3, FINSEQ_1:77;
hence phi . <*h,k*> = h * k by B3; :: thesis: verum

end;

hence for h, k being Element of G st h in H & k in K holds
phi . <*h,k*> = h * k ; :: thesis: ( phi is one-to-one iff H /\ K = (1). G )
the carrier of (product <*H,K*>) = product (Carrier <*H,K*>) by GROUP_7:def 2;
hence ( phi is one-to-one iff H /\ K = (1). G ) by A3, Th58; :: thesis: verum