let G be Group; :: thesis: for H, K being Subgroup of G st H is Subgroup of K holds
for N being normal Subgroup of G st N is Subgroup of K holds
( H,(K,N) `*` are_complements_in K iff ( N * H = 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 normal Subgroup of G st N is Subgroup of K holds
( H,(K,N) `*` are_complements_in K iff ( N * H = the carrier of K & H /\ N = (1). K ) ) )
assume A1: H is Subgroup of K ; :: thesis: for N being normal Subgroup of G st N is Subgroup of K holds
( H,(K,N) `*` are_complements_in K iff ( N * H = the carrier of K & H /\ N = (1). K ) )
then reconsider H1 = multMagma(# the carrier of H, the multF of H #) as strict Subgroup of K by Th1;
let N be normal Subgroup of G; :: thesis: ( N is Subgroup of K implies ( H,(K,N) `*` are_complements_in K iff ( N * H = the carrier of K & H /\ N = (1). K ) ) )
assume N is Subgroup of K ; :: thesis: ( H,(K,N) `*` are_complements_in K iff ( N * H = the carrier of K & H /\ N = (1). K ) )
then A2: N is normal Subgroup of K by GROUP_6:8;
then multMagma(# the carrier of ((K,N) `*`), the multF of ((K,N) `*`) #) = multMagma(# the carrier of N, the multF of N #) by Th41;
then ( H1,(K,N) `*` are_complements_in K iff H,N are_complements_in K ) ;
hence ( H,(K,N) `*` are_complements_in K iff ( N * H = the carrier of K & H /\ N = (1). K ) ) by A1, A2, Th43; :: thesis: verum