reconsider H = multMagma(# the carrier of N, the multF of N #) as strict normal Subgroup of G by Lm6;
set x = Cosets H;
take Cosets H ; :: thesis: for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
Cosets H = Cosets H
let H be strict normal Subgroup of G; :: thesis: ( H = multMagma(# the carrier of N, the multF of N #) implies Cosets H = Cosets H )
assume H = multMagma(# the carrier of N, the multF of N #) ; :: thesis: Cosets H = Cosets H
hence Cosets H = Cosets H ; :: thesis: verum