theorem Th43: :: VECTSP11:43

for K being Field
for V1, V2 being VectSp of K
for L being Linear_Combination of V1
for F being FinSequence of V1
for f being linear-transformation of V1,V2 st f | ((Carrier L) /\ (rng F)) is one-to-one & rng F c= Carrier L holds
ex Lf being Linear_Combination of V2 st
( Carrier Lf = f .: ((Carrier L) /\ (rng F)) & f * (L (#) F) = Lf (#) (f * F) & ( for v1 being Vector of V1 st v1 in (Carrier L) /\ (rng F) holds
L . v1 = Lf . (f . v1) ) )