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

A1: now :: thesis: for z being Element of INT
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 INT ; :: 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 ZMODUL01:def 13;
reconsider c = (z * a) + W as Coset of W by ZMODUL01:def 13;
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, ZMODUL01:58;
then consider w1 being VECTOR of V such that
A4: ( w1 in W & a1 = a + w1 ) by ZMODUL01:72;
( z * a1 = (z * a) + (z * w1) & z * w1 in W ) by A4, ZMODUL01:def 2, ZMODUL01:37;
then A5: z * a1 in (z * a) + W ;
z * a1 in (z * a1) + W by ZMODUL01:58;
hence c = (z * a1) + W by A5, ZMODUL01:68; :: thesis: verum

end;

end;

consider f being Function of [:INT,(CosetSet (V,W)):],(CosetSet (V,W)) such that
A6: for z being Element of INT
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 Integer
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 Integer; :: 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 A7: A = a + W ; :: thesis: f . (z,A) = (z * a) + W
reconsider z = z as Element of INT by INT_1:def 2;
S₁[z,A,f . (z,A)] by A6;
hence f . (z,A) = (z * a) + W by A7; :: thesis: verum