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

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