set C = CosetSet (V,W);
let f1, f2 be BinOp of (CosetSet (V,W)); :: thesis: ( ( 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 ; :: thesis: f1 = f2

now :: thesis: 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); :: thesis: 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 ; :: thesis: verum

end;

hence f1 = f2 by BINOP_1:2; :: thesis: verum