let G be Group; :: thesis: for H, K being Subgroup of G st H is Subgroup of K holds
for N being Subgroup of G st N is normal Subgroup of K holds
( H,N are_complements_in K iff ( H * N = the carrier of K & H /\ N = (1). K ) )
let H, K be Subgroup of G; :: thesis: ( H is Subgroup of K implies for N being Subgroup of G st N is normal Subgroup of K holds
( H,N are_complements_in K iff ( H * N = the carrier of K & H /\ N = (1). K ) ) )
assume A1: H is Subgroup of K ; :: thesis: for N being Subgroup of G st N is normal Subgroup of K holds
( H,N are_complements_in K iff ( H * N = the carrier of K & H /\ N = (1). K ) )
let N be Subgroup of G; :: thesis: ( N is normal Subgroup of K implies ( H,N are_complements_in K iff ( H * N = the carrier of K & H /\ N = (1). K ) ) )
assume A2: N is normal Subgroup of K ; :: thesis: ( H,N are_complements_in K iff ( H * N = the carrier of K & H /\ N = (1). K ) )
then N * H = H * N by A1, Th40;
hence ( H,N are_complements_in K iff ( H * N = the carrier of K & H /\ N = (1). K ) ) by A1, A2, Th43; :: thesis: verum