reconsider H = multMagma(# the carrier of N, the multF of N #) as strict normal Subgroup of G by Lm6;

Cosets N = Cosets H by Def14;

then reconsider x = CosOp H as BinOp of (Cosets N) ;

take x ; :: thesis: for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds

x = CosOp H

let H be strict normal Subgroup of G; :: thesis: ( H = multMagma(# the carrier of N, the multF of N #) implies x = CosOp H )

assume H = multMagma(# the carrier of N, the multF of N #) ; :: thesis: x = CosOp H

hence x = CosOp H ; :: thesis: verum

Cosets N = Cosets H by Def14;

then reconsider x = CosOp H as BinOp of (Cosets N) ;

take x ; :: thesis: for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds

x = CosOp H

let H be strict normal Subgroup of G; :: thesis: ( H = multMagma(# the carrier of N, the multF of N #) implies x = CosOp H )

assume H = multMagma(# the carrier of N, the multF of N #) ; :: thesis: x = CosOp H

hence x = CosOp H ; :: thesis: verum