let LCL1, LCL2 be BinOp of (Cosets N); ( ( for H1, H2 being Element of Cosets N holds LCL1 . (H1,H2) = H1 * H2 ) & ( for H1, H2 being Element of Cosets N holds LCL2 . (H1,H2) = H1 * H2 ) implies LCL1 = LCL2 )
assume that
A5:
for H1, H2 being Element of Cosets N holds LCL1 . (H1,H2) = H1 * H2
and
A6:
for H1, H2 being Element of Cosets N holds LCL2 . (H1,H2) = H1 * H2
; LCL1 = LCL2
for H1, H2 being Element of Cosets N holds LCL1 . (H1,H2) = LCL2 . (H1,H2)
proof
let H1,
H2 be
Element of
Cosets N;
LCL1 . (H1,H2) = LCL2 . (H1,H2)
LCL1 . (
H1,
H2) =
H1 * H2
by A5
.=
LCL2 . (
H1,
H2)
by A6
;
hence
LCL1 . (
H1,
H2)
= LCL2 . (
H1,
H2)
;
verum
end;
hence
LCL1 = LCL2
; verum