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

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