set C = CosetSet (V,W);
let f1, f2 be BinOp of (CosetSet (V,W)); ( ( for A, B being Element of CosetSet (V,W)
for a, b being Vector of V st A = a + W & B = b + W holds
f1 . (A,B) = (a + b) + W ) & ( for A, B being Element of CosetSet (V,W)
for a, b being Vector of V st A = a + W & B = b + W holds
f2 . (A,B) = (a + b) + W ) implies f1 = f2 )
assume that
A15:
for A, B being Element of CosetSet (V,W)
for a, b being Vector of V st A = a + W & B = b + W holds
f1 . (A,B) = (a + b) + W
and
A16:
for A, B being Element of CosetSet (V,W)
for a, b being Vector of V st A = a + W & B = b + W holds
f2 . (A,B) = (a + b) + W
; f1 = f2
now for A, B being Element of CosetSet (V,W) holds f1 . (A,B) = f2 . (A,B)let A,
B be
Element of
CosetSet (
V,
W);
f1 . (A,B) = f2 . (A,B)
A in CosetSet (
V,
W)
;
then consider A1 being
Coset of
W such that A17:
A1 = A
;
consider a being
Vector of
V such that A18:
A1 = a + W
by VECTSP_4:def 6;
B in CosetSet (
V,
W)
;
then consider B1 being
Coset of
W such that A19:
B1 = B
;
consider b being
Vector of
V such that A20:
B1 = b + W
by VECTSP_4:def 6;
thus f1 . (
A,
B) =
(a + b) + W
by A15, A17, A19, A18, A20
.=
f2 . (
A,
B)
by A16, A17, A19, A18, A20
;
verum end;
hence
f1 = f2
by BINOP_1:2; verum