defpred S₁[ Element of V, Element of (VectQuot (V,W))] means $2 = $1 + W;
A11: for v being Element of V ex y being Element of (VectQuot (V,W)) st S₁[v,y]

proof

let v be Element of V; :: thesis: ex y being Element of (VectQuot (V,W)) st S₁[v,y]
reconsider y = v + W as Coset of W by VECTSP_4:def 6;
y in CosetSet (V,W) ;
then reconsider y = y as Element of (VectQuot (V,W)) by VECTSP10:def 6;
take y ; :: thesis: S₁[v,y]
thus S₁[v,y] ; :: thesis: verum

end;

consider f being Function of V,(VectQuot (V,W)) such that
A15: for v being Element of V holds S₁[v,f . v] from FUNCT_2:sch 3(A11);
for x, y being Vector of V holds f . (x + y) = (f . x) + (f . y)

proof

let x, y be Vector of V; :: thesis: f . (x + y) = (f . x) + (f . y)
A2: f . x = x + W by A15;
A3: f . y = y + W by A15;
reconsider A = x + W as Element of CosetSet (V,W) by A2, VECTSP10:def 6;
reconsider B = y + W as Element of CosetSet (V,W) by A3, VECTSP10:def 6;
thus f . (x + y) = (x + y) + W by A15
.= (addCoset (V,W)) . (A,B) by VECTSP10:def 3
.= (f . x) + (f . y) by A2, A3, VECTSP10:def 6 ; :: thesis: verum

end;

then A16: f is additive ;
for a being Element of R
for x being Element of V holds f . (a * x) = a * (f . x)

proof

let a be Element of R; :: thesis: for x being Element of V holds f . (a * x) = a * (f . x)
let x be Element of V; :: thesis: f . (a * x) = a * (f . x)
A2: f . x = x + W by A15;
reconsider A = x + W as Element of CosetSet (V,W) by A2, VECTSP10:def 6;
thus f . (a * x) = (a * x) + W by A15
.= (lmultCoset (V,W)) . (a,A) by VECTSP10:def 5
.= a * (f . x) by A2, VECTSP10:def 6 ; :: thesis: verum

end;

then f is homogeneous ;
hence ex b₁ being linear-transformation of V,(VectQuot (V,W)) st
for v being Element of V holds b₁ . v = v + W by A15, A16; :: thesis: verum