defpred S₁[ set , set , set ] means for a, b being Vector of V st $1 = a + W & $2 = b + W holds
$3 = (a + b) + W;
set C = CosetSet (V,W);

A1: now :: thesis: for A, B being Element of CosetSet (V,W) ex z being Element of CosetSet (V,W) st S₁[A,B,z]

let A, B be Element of CosetSet (V,W); :: thesis: ex z being Element of CosetSet (V,W) st S₁[A,B,z]
A in CosetSet (V,W) ;
then consider A1 being Coset of W such that
A2: A1 = A ;
consider a being Vector of V such that
A3: A1 = a + W by VECTSP_4:def 6;
B in CosetSet (V,W) ;
then consider B1 being Coset of W such that
A4: B1 = B ;
consider b being Vector of V such that
A5: B1 = b + W by VECTSP_4:def 6;
reconsider z = (a + b) + W as Coset of W by VECTSP_4:def 6;
z in CosetSet (V,W) ;
then reconsider z = z as Element of CosetSet (V,W) ;
take z = z; :: thesis: S₁[A,B,z]
thus S₁[A,B,z] :: thesis: verum

proof

let a1, b1 be Vector of V; :: thesis: ( A = a1 + W & B = b1 + W implies z = (a1 + b1) + W )
assume that
A6: A = a1 + W and
A7: B = b1 + W ; :: thesis: z = (a1 + b1) + W
a1 in a + W by A2, A3, A6, VECTSP_4:44;
then consider w1 being Vector of V such that
A8: w1 in W and
A9: a1 = a + w1 by VECTSP_4:42;
b1 in b + W by A4, A5, A7, VECTSP_4:44;
then consider w2 being Vector of V such that
A10: w2 in W and
A11: b1 = b + w2 by VECTSP_4:42;
A12: w1 + w2 in W by A8, A10, VECTSP_4:20;
a1 + b1 = ((w1 + a) + b) + w2 by A9, A11, RLVECT_1:def 3
.= (w1 + (a + b)) + w2 by RLVECT_1:def 3
.= (a + b) + (w1 + w2) by RLVECT_1:def 3 ;
then A13: a1 + b1 in (a + b) + W by A12;
a1 + b1 in (a1 + b1) + W by VECTSP_4:44;
hence z = (a1 + b1) + W by A13, VECTSP_4:56; :: thesis: verum

end;

end;

consider f being Function of [:(CosetSet (V,W)),(CosetSet (V,W)):],(CosetSet (V,W)) such that
A14: for A, B being Element of CosetSet (V,W) holds S₁[A,B,f . (A,B)] from BINOP_1:sch 3(A1);
reconsider f = f as BinOp of (CosetSet (V,W)) ;
take f ; :: 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
f . (A,B) = (a + b) + W
let A, B be Element of CosetSet (V,W); :: thesis: for a, b being Vector of V st A = a + W & B = b + W holds
f . (A,B) = (a + b) + W
let a, b be Vector of V; :: thesis: ( A = a + W & B = b + W implies f . (A,B) = (a + b) + W )
assume ( A = a + W & B = b + W ) ; :: thesis: f . (A,B) = (a + b) + W
hence f . (A,B) = (a + b) + W by A14; :: thesis: verum