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