let F be Field; :: thesis: for V, W being VectSp of F
for T being linear-transformation of V,W
for X being Subset of V
for l being Linear_Combination of T .: X st T | X is one-to-one holds
T @ (T # l) = l

let V, W be VectSp of F; :: thesis: for T being linear-transformation of V,W
for X being Subset of V
for l being Linear_Combination of T .: X st T | X is one-to-one holds
T @ (T # l) = l

let T be linear-transformation of V,W; :: thesis: for X being Subset of V
for l being Linear_Combination of T .: X st T | X is one-to-one holds
T @ (T # l) = l

let X be Subset of V; :: thesis: for l being Linear_Combination of T .: X st T | X is one-to-one holds
T @ (T # l) = l

let l be Linear_Combination of T .: X; :: thesis: ( T | X is one-to-one implies T @ (T # l) = l )
assume A1: T | X is one-to-one ; :: thesis: T @ (T # l) = l
let w be Element of W; :: according to FUNCT_2:def 8 :: thesis: (T @ (T # l)) . w = l . w
set m = T @ (T # l);
per cases ( w in Carrier l or not w in Carrier l ) ;
suppose A2: w in Carrier l ; :: thesis: (T @ (T # l)) . w = l . w
then A3: l . w <> 0. F by VECTSP_6:2;
A4: dom (T # l) = [#] V by FUNCT_2:92;
Carrier l c= T .: X by VECTSP_6:def 4;
then consider v being object such that
A5: v in dom T and
A6: v in X and
A7: w = T . v by ;
reconsider v = v as Element of V by A5;
consider B being Subset of V such that
A8: B misses X and
A9: T " {(T . v)} = {v} \/ B by A1, A6, Th34;
A10: (T # l) . v = l . (T . v) by A1, A6, Th42;
A11: (T # l) .: {v} = Im ((T # l),v)
.= {((T # l) . v)} by ;
A12: (T @ (T # l)) . w = Sum ((T # l) .: (T " {(T . v)})) by
.= Sum ({(l . (T . v))} \/ ((T # l) .: B)) by ;
per cases ( B = {} or B <> {} ) ;
suppose B = {} ; :: thesis: (T @ (T # l)) . w = l . w
then (T @ (T # l)) . w = Sum ({(l . (T . v))} \/ ({} F)) by A12
.= l . w by ;
hence (T @ (T # l)) . w = l . w ; :: thesis: verum
end;
suppose A13: B <> {} ; :: thesis: (T @ (T # l)) . w = l . w
Carrier (T # l) c= X by VECTSP_6:def 4;
then B misses Carrier (T # l) by ;
then (T @ (T # l)) . w = Sum ({(l . (T . v))} \/ {(0. F)}) by
.= (Sum {(l . (T . v))}) + (Sum {(0. F)}) by
.= (l . (T . v)) + (Sum {(0. F)}) by RLVECT_2:9
.= (l . (T . v)) + (0. F) by RLVECT_2:9
.= l . w by ;
hence (T @ (T # l)) . w = l . w ; :: thesis: verum
end;
end;
end;
suppose A14: not w in Carrier l ; :: thesis: (T @ (T # l)) . w = l . w
then A15: l . w = 0. F ;
now :: thesis: not (T @ (T # l)) . w <> 0. F
assume A16: (T @ (T # l)) . w <> 0. F ; :: thesis: contradiction
then w in Carrier (T @ (T # l)) ;
then T " {w} meets Carrier (T # l) by Th36;
then consider v being Element of V such that
A17: v in T " {w} and
A18: v in Carrier (T # l) by Th3;
T . v in {w} by ;
then A19: T . v = w by TARSKI:def 1;
A20: Carrier (T # l) c= X by VECTSP_6:def 4;
then T | (Carrier (T # l)) is one-to-one by ;
then (T @ (T # l)) . w = (T # l) . v by
.= 0. F by A1, A15, A18, A19, A20, Th42 ;
hence contradiction by A16; :: thesis: verum
end;
hence (T @ (T # l)) . w = l . w by A14; :: thesis: verum
end;
end;