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 A1: 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 )
assume A2: 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
reconsider H = multMagma(# the carrier of N,the multF of N #) as strict normal Subgroup of G by Lm7;
y1 = CosOp H by A1;
hence y1 = y2 by A2; :: thesis: verum