let F be Field; :: thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V
for v being Element of V st T | (Carrier l) is one-to-one & v in Carrier l holds
(T @ l) . (T . v) = l . v
let W, V be VectSp of F; :: thesis: for T being linear-transformation of V,W
for l being Linear_Combination of V
for v being Element of V st T | (Carrier l) is one-to-one & v in Carrier l holds
(T @ l) . (T . v) = l . v
let T be linear-transformation of V,W; :: thesis: for l being Linear_Combination of V
for v being Element of V st T | (Carrier l) is one-to-one & v in Carrier l holds
(T @ l) . (T . v) = l . v
let l be Linear_Combination of V; :: thesis: for v being Element of V st T | (Carrier l) is one-to-one & v in Carrier l holds
(T @ l) . (T . v) = l . v
let v be Element of V; :: thesis: ( T | (Carrier l) is one-to-one & v in Carrier l implies (T @ l) . (T . v) = l . v )
assume that
A1: T | (Carrier l) is one-to-one and
A2: v in Carrier l ; :: thesis: (T @ l) . (T . v) = l . v
consider X being Subset of V such that
A3: X misses Carrier l and
A4: T " {(T . v)} = {v} \/ X by A1, A2, Th34;

per cases ( X = {} or X <> {} ) ;

suppose A5: X = {} ; :: thesis: (T @ l) . (T . v) = l . v

A6: dom l = [#] V by FUNCT_2:169;
l .: {v} = Im l,v
.= {(l . v)} by A6, FUNCT_1:117 ;
then Sum (l .: (T " {(T . v)})) = l . v by A4, A5, RLVECT_2:15;
hence (T @ l) . (T . v) = l . v by Def5; :: thesis: verum

end;

suppose A7: X <> {} ; :: thesis: (T @ l) . (T . v) = l . v

A8: l .: (T " {(T . v)}) = (l .: {v}) \/ (l .: X) by A4, RELAT_1:153;
A9: dom l = [#] V by FUNCT_2:169;
A10: l .: {v} = Im l,v
.= {(l . v)} by A9, FUNCT_1:117 ;
A11: l .: X = {(0. F)}

proof

A12: {(0. F)} c= l .: X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. F)} or x in l .: X )
assume A13: x in {(0. F)} ; :: thesis: x in l .: X
A14: x = 0. F by A13, TARSKI:def 1;
consider y being set such that
A15: y in X by A7, XBOOLE_0:def 1;

A16: now

assume y in Carrier l ; :: thesis: contradiction
then y in (Carrier l) /\ X by A15, XBOOLE_0:def 4;
hence contradiction by A3, XBOOLE_0:def 7; :: thesis: verum

end;

reconsider y = y as Element of V by A15;
l . y = x by A14, A16;
hence x in l .: X by A9, A15, FUNCT_1:def 12; :: thesis: verum

end;

l .: X c= {(0. F)}

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in l .: X or y in {(0. F)} )
assume A17: y in l .: X ; :: thesis: y in {(0. F)}
consider x being set such that
A18: x in dom l and
A19: x in X and
A20: y = l . x by A17, FUNCT_1:def 12;

A21: now

assume x in Carrier l ; :: thesis: contradiction
then x in (Carrier l) /\ X by A19, XBOOLE_0:def 4;
hence contradiction by A3, XBOOLE_0:def 7; :: thesis: verum

end;

reconsider x = x as Element of V by A18;
l . x = 0. F by A21;
hence y in {(0. F)} by A20, TARSKI:def 1; :: thesis: verum

end;

hence l .: X = {(0. F)} by A12, XBOOLE_0:def 10; :: thesis: verum

end;

l .: X misses l .: {v}

proof

A22: dom l = [#] V by FUNCT_2:169;
A23: l .: {v} = Im l,v
.= {(l . v)} by A22, FUNCT_1:117 ;
assume l .: X meets l .: {v} ; :: thesis: contradiction
then consider x being set such that
A24: x in l .: X and
A25: x in l .: {v} by XBOOLE_0:3;
A26: x = 0. F by A11, A24, TARSKI:def 1;
x = l . v by A23, A25, TARSKI:def 1;
hence contradiction by A2, A26, VECTSP_6:20; :: thesis: verum

end;

then Sum (l .: (T " {(T . v)})) = (Sum (l .: {v})) + (Sum (l .: X)) by A8, RLVECT_2:18
.= (l . v) + (Sum {(0. F)}) by A10, A11, RLVECT_2:15
.= (l . v) + (0. F) by RLVECT_2:15
.= l . v by RLVECT_1:10 ;
hence (T @ l) . (T . v) = l . v by Def5; :: thesis: verum

end;

end;