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
N * H = H * N
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
N * H = H * N )
assume H is Subgroup of K ; :: thesis: for N being Subgroup of G st N is normal Subgroup of K holds
N * H = H * N
then reconsider H0 = H as Subgroup of K ;
let N be Subgroup of G; :: thesis: ( N is normal Subgroup of K implies N * H = H * N )
assume N is normal Subgroup of K ; :: thesis: N * H = H * N
then reconsider N0 = N as normal Subgroup of K ;
A1: multMagma(# the carrier of N0, the multF of N0 #) = multMagma(# the carrier of N, the multF of N #) ;
A2: multMagma(# the carrier of H0, the multF of H0 #) = multMagma(# the carrier of H, the multF of H #) ;
hence N * H = N0 * H0 by ThProdLemma, A1
.= H0 * N0 by GROUP_5:8
.= H * N by ThProdLemma, A1, A2 ;
:: thesis: verum