reconsider H = multMagma(# the carrier of N, the multF of N #) as strict normal Subgroup of G by Lm6;
let y1, y2 be BinOp of (Cosets N); :: thesis: ( ( for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
y1 = CosOp H ) & ( for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
y2 = CosOp H ) implies y1 = y2 )
assume for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
y1 = CosOp H ; :: thesis: ( ex H being strict normal Subgroup of G st
( H = multMagma(# the carrier of N, the multF of N #) & not y2 = CosOp H ) or y1 = y2 )
then A1: y1 = CosOp H ;
assume for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
y2 = CosOp H ; :: thesis: y1 = y2
hence y1 = y2 by A1; :: thesis: verum