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
A11: for A being Vector of (VectQuot V,W)
for a being Vector of V st A = a + W holds
f1 . A = f . a and
A12: 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

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

end;

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