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

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:59;
then consider w1 being Vector of V such that
A4: ( w1 in W & a1 = a + w1 ) by VECTSP_4:57;
( z * a1 = (z * a) + (z * w1) & z * w1 in W ) by A4, VECTSP_1:def 26, VECTSP_4:29;
then A5: z * a1 in (z * a) + W ;
z * a1 in (z * a1) + W by VECTSP_4:59;
hence c = (z * a1) + W by A5, VECTSP_4:71; :: 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