set vq = VectQuot (V,W);
let f1, f2 be linear-transformation of (VectQuot (V,W)),U; :: 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 VECTSP10:22;
thus f1 . A = f . a by A12, A14
.= f2 . A by A13, A14 ; :: thesis: verum
end;
hence f1 = f2 ; :: thesis: verum