theorem canlinsurj3: :: VECTSP13:20

for F being Field
for U being non trivial finite-dimensional VectSp of F
for V being finite-dimensional VectSp of F
for B being Basis of U
for f being Function of B,V
for l2 being Linear_Combination of rng f ex l1 being Linear_Combination of B st (canLinTrans f) . (Sum l1) = Sum l2