set vq = VectQuot (V,W);
let f1, f2 be additive Functional of (VectQuot (V,W)); :: thesis: ( ( for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
f1 . A = f . a ) & ( for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
f2 . A = f . a ) implies f1 = f2 )
assume that
A12: for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
f1 . A = f . a and
A13: for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
f2 . A = f . a ; :: thesis: f1 = f2

now :: thesis: for A being Vector of (VectQuot (V,W)) holds f1 . A = f2 . A

let A be Vector of (VectQuot (V,W)); :: thesis: f1 . A = f2 . A
consider a being Vector of V such that
A14: A = a + W by Th22;
thus f1 . A = f . a by A12, A14
.= f2 . A by A13, A14 ; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:63; :: thesis: verum