defpred S₁[ Element of K, set , set ] means for a being Vector of V st $2 = a + W holds
$3 = ($1 * a) + W;
set cF = the carrier of K;
set C = CosetSet (V,W);

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

let z be Element of K; :: thesis: for A being Element of CosetSet (V,W) ex c being Element of CosetSet (V,W) st S₁[z,A,c]
let A be Element of CosetSet (V,W); :: thesis: ex c being Element of CosetSet (V,W) st S₁[z,A,c]
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;
reconsider c = (z * a) + W as Coset of W by VECTSP_4:def 6;
c in CosetSet (V,W) ;
then reconsider c = c as Element of CosetSet (V,W) ;
take c = c; :: thesis: S₁[z,A,c]
thus S₁[z,A,c] :: thesis: verum

proof

let a1 be Vector of V; :: thesis: ( A = a1 + W implies c = (z * a1) + W )
assume A = a1 + W ; :: thesis: c = (z * a1) + W
then a1 in a + W by A2, A3, VECTSP_4:44;
then consider w1 being Vector of V such that
A4: ( w1 in W & a1 = a + w1 ) by VECTSP_4:42;
( z * a1 = (z * a) + (z * w1) & z * w1 in W ) by A4, VECTSP_1:def 14, VECTSP_4:21;
then A5: z * a1 in (z * a) + W ;
z * a1 in (z * a1) + W by VECTSP_4:44;
hence c = (z * a1) + W by A5, VECTSP_4:56; :: thesis: verum

end;

end;

consider f being Function of [: the carrier of K,(CosetSet (V,W)):],(CosetSet (V,W)) such that
A6: for z being Element of K
for A being Element of CosetSet (V,W) holds S₁[z,A,f . (z,A)] from BINOP_1:sch 3(A1);
take f ; :: thesis: for z being Element of K
for A being Element of CosetSet (V,W)
for a being Vector of V st A = a + W holds
f . (z,A) = (z * a) + W
let z be Element of K; :: thesis: for A being Element of CosetSet (V,W)
for a being Vector of V st A = a + W holds
f . (z,A) = (z * a) + W
let A be Element of CosetSet (V,W); :: thesis: for a being Vector of V st A = a + W holds
f . (z,A) = (z * a) + W
let a be Vector of V; :: thesis: ( A = a + W implies f . (z,A) = (z * a) + W )
assume A = a + W ; :: thesis: f . (z,A) = (z * a) + W
hence f . (z,A) = (z * a) + W by A6; :: thesis: verum