defpred S₁[ set , set ] means for a being Vector of V st $1 = a + W holds
$2 = f . a;
set aC = addCoset (V,W);
set C = CosetSet (V,W);
set vq = VectQuot (V,W);

A2: now :: thesis: for A being Vector of (VectQuot (V,W)) ex y being Element of the carrier of U st S₁[A,y]

let A be Vector of (VectQuot (V,W)); :: thesis: ex y being Element of the carrier of U st S₁[A,y]
consider a being Vector of V such that
A3: A = a + W by VECTSP10:22;
take y = f . a; :: thesis: S₁[A,y]
thus S₁[A,y] :: thesis: verum

proof

let a1 be Vector of V; :: thesis: ( A = a1 + W implies y = f . a1 )
assume A = a1 + W ; :: thesis: y = f . a1
then consider w being Vector of V such that
A4: w in W and
A5: a = a1 + w by A3, VECTSP_4:42, VECTSP_4:44;
w in ker f by A1, A4;
then A6: f . w = 0. U by RANKNULL:10;
thus y = (f . a1) + (f . w) by A5, VECTSP_1:def 20
.= f . a1 by A6 ; :: thesis: verum

end;

end;

consider ff being Function of the carrier of (VectQuot (V,W)), the carrier of U such that
A7: for A being Vector of (VectQuot (V,W)) holds S₁[A,ff . A] from FUNCT_2:sch 3(A2);
reconsider ff = ff as Function of (VectQuot (V,W)),U ;
A8: CosetSet (V,W) = the carrier of (VectQuot (V,W)) by VECTSP10:def 6;

now :: thesis: for A, B being Vector of (VectQuot (V,W)) holds ff . (A + B) = (ff . A) + (ff . B)

A9: the addF of (VectQuot (V,W)) = addCoset (V,W) by VECTSP10:def 6;
let A, B be Vector of (VectQuot (V,W)); :: thesis: ff . (A + B) = (ff . A) + (ff . B)
consider a being Vector of V such that
A10: A = a + W by VECTSP10:22;
consider b being Vector of V such that
A11: B = b + W by VECTSP10:22;
(addCoset (V,W)) . (A,B) = (a + b) + W by A8, A10, A11, VECTSP10:def 3;
hence ff . (A + B) = f . (a + b) by A7, A9
.= (f . a) + (f . b) by VECTSP_1:def 20
.= (ff . A) + (f . b) by A7, A10
.= (ff . A) + (ff . B) by A7, A11 ;
:: thesis: verum

end;

then AD: ff is additive ;

now :: thesis: for A being Vector of (VectQuot (V,W))
for r being Element of K holds ff . (r * A) = r * (ff . A)

let A be Vector of (VectQuot (V,W)); :: thesis: for r being Element of K holds ff . (r * A) = r * (ff . A)
let r be Element of K; :: thesis: ff . (r * A) = r * (ff . A)
A2: CosetSet (V,W) = the carrier of (VectQuot (V,W)) by VECTSP10:def 6;
then A in CosetSet (V,W) ;
then consider aa being Coset of W such that
A3: A = aa ;
consider a being Vector of V such that
A4: aa = a + W by VECTSP_4:def 6;
r * A = (lmultCoset (V,W)) . (r,A) by VECTSP10:def 6
.= (r * a) + W by A2, A3, A4, VECTSP10:def 5 ;
hence ff . (r * A) = f . (r * a) by A7
.= r * (f . a) by MOD_2:def 2
.= r * (ff . A) by A3, A4, A7 ;
:: thesis: verum

end;

then ff is homogeneous ;
then reconsider ff = ff as linear-transformation of (VectQuot (V,W)),U by AD;
take ff ; :: thesis: for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
ff . A = f . a
thus for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
ff . A = f . a by A7; :: thesis: verum