let LCL1, LCL2 be BinOp of (Cosets N); :: thesis: ( ( 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 ; :: thesis: 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; :: thesis: 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) ; :: thesis: verum

end;

hence LCL1 = LCL2 ; :: thesis: verum