let G be Group; :: thesis: for H, K being normal Subgroup of G st H /\ K = (1). G holds
for h, k being Element of G st h in H & k in K holds
h * k = k * h
let H, K be normal Subgroup of G; :: thesis: ( H /\ K = (1). G implies for h, k being Element of G st h in H & k in K holds
h * k = k * h )
assume A1: H /\ K = (1). G ; :: thesis: for h, k being Element of G st h in H & k in K holds
h * k = k * h
let h, k be Element of G; :: thesis: ( h in H & k in K implies h * k = k * h )
assume A2: h in H ; :: thesis: ( not k in K or h * k = k * h )
assume A3: k in K ; :: thesis: h * k = k * h
[.h,k.] in H /\ K

proof

A4: [.h,k.] in H

proof

( h " in H & h |^ k in H ) by A2, ThNorm, GROUP_2:51;
then (h ") * (h |^ k) in H by GROUP_2:50;
hence [.h,k.] in H by GROUP_5:18; :: thesis: verum

end;

[.h,k.] in K

proof

k " in K by A3, GROUP_2:51;
then (k ") |^ h in K by ThNorm;
then ((k ") |^ h) * k in K by A3, GROUP_2:50;
hence [.h,k.] in K by GROUP_5:18; :: thesis: verum

end;

hence [.h,k.] in H /\ K by A4, GROUP_2:82; :: thesis: verum

end;

then 1_ G = [.h,k.] by A1, GROUP_5:1;
hence h * k = k * h by GROUP_5:36; :: thesis: verum