let R be Ring; :: thesis: for V, W being LeftMod of R
for X being Subset of V
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 LeftMod of R; :: thesis: for X being Subset of V
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 X be Subset of V; :: 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 VECTSP_6:def 7 :: thesis: (T @* (T # l)) . w = l . w
set m = T @* (T # l);
reconsider SZ0 = {(0. R)} as finite Subset of R ;
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
Carrier l c= T .: X by VECTSP_6:def 4;
then consider v being object such that
A3: v in dom T and
A4: v in X and
A5: w = T . v by ;
reconsider v = v as Element of V by A3;
w in the carrier of W ;
then A6: w in dom l by FUNCT_2:def 1;
A7: v in the carrier of V ;
for x being object holds
( x in (T " {w}) /\ (Carrier (T # l)) iff x in {v} /\ (Carrier (T # l)) )
proof
let x be object ; :: thesis: ( x in (T " {w}) /\ (Carrier (T # l)) iff x in {v} /\ (Carrier (T # l)) )
hereby :: thesis: ( x in {v} /\ (Carrier (T # l)) implies x in (T " {w}) /\ (Carrier (T # l)) )
assume A8: x in (T " {w}) /\ (Carrier (T # l)) ; :: thesis: x in {v} /\ (Carrier (T # l))
then A9: ( x in T " {w} & x in Carrier (T # l) ) by XBOOLE_0:def 4;
then A10: x in X by ;
x in the carrier of V by A8;
then A11: x in dom T by FUNCT_2:def 1;
A12: ( x in the carrier of V & T . x in {w} ) by ;
A13: (T | X) . x = T . x by
.= T . v by
.= (T | X) . v by ;
A14: x in dom (T | X) by ;
v in dom (T | X) by ;
then x = v by ;
then x in {v} by TARSKI:def 1;
hence x in {v} /\ (Carrier (T # l)) by ; :: thesis: verum
end;
assume x in {v} /\ (Carrier (T # l)) ; :: thesis: x in (T " {w}) /\ (Carrier (T # l))
then A15: ( x in {v} & x in Carrier (T # l) ) by XBOOLE_0:def 4;
then A16: x = v by TARSKI:def 1;
( x in the carrier of V & T . x in {w} ) by ;
then x in T " {w} by FUNCT_2:38;
hence x in (T " {w}) /\ (Carrier (T # l)) by ; :: thesis: verum
end;
then A17: (T " {w}) /\ (Carrier (T # l)) = {v} /\ (Carrier (T # l)) by TARSKI:2;
per cases ( not v in Carrier (T # l) or v in Carrier (T # l) ) ;
suppose A18: not v in Carrier (T # l) ; :: thesis: (T @* (T # l)) . w = l . w
{v} /\ (Carrier (T # l)) = {}
proof
assume {v} /\ (Carrier (T # l)) <> {} ; :: thesis: contradiction
then consider x being object such that
A19: x in {v} /\ (Carrier (T # l)) by XBOOLE_0:def 1;
A20: x in {v} by ;
x in Carrier (T # l) by ;
hence contradiction by A18, A20, TARSKI:def 1; :: thesis: verum
end;
then b1: lCFST ((T # l),T,w) = <*> the carrier of R by A17;
(T @* (T # l)) . w = Sum (lCFST ((T # l),T,w)) by LDef5;
then A21: (T @* (T # l)) . w = 0. R by ;
A22: (T # l) . v = 0. R by A18;
A23: not v in dom ((X `) --> (0. R)) by ;
T # l = (l * T) +* ((X `) --> (0. R)) by ;
then (T # l) . v = (l * T) . v by ;
hence (T @* (T # l)) . w = l . w by ; :: thesis: verum
end;
suppose v in Carrier (T # l) ; :: thesis: (T @* (T # l)) . w = l . w
then (T " {w}) /\ (Carrier (T # l)) = {v} by ;
then A24: canFS ((T " {w}) /\ (Carrier (T # l))) = <*v*> by FINSEQ_1:94;
A25: not v in dom ((X `) --> (0. R)) by ;
A26: T # l = (l * T) +* ((X `) --> (0. R)) by ;
A27: v in dom (T # l) by ;
A28: v in dom (l * T) by ;
(T # l) * <*v*> = <*((T # l) . v)*> by
.= <*((l * T) . v)*> by
.= (l * T) * <*v*> by
.= l * (T * <*v*>) by RELAT_1:36
.= l * <*(T . v)*> by
.= <*(l . w)*> by ;
then Sum (lCFST ((T # l),T,w)) = l . w by ;
hence (T @* (T # l)) . w = l . w by LDef5; :: thesis: verum
end;
end;
end;
suppose A29: not w in Carrier l ; :: thesis: (T @* (T # l)) . w = l . w
then A30: l . w = 0. R ;
now :: thesis: not (T @* (T # l)) . w <> 0. R
assume A31: (T @* (T # l)) . w <> 0. R ; :: thesis: contradiction
then w in Carrier (T @* (T # l)) ;
then consider v being Element of V such that
A32: v in T " {w} and
A33: v in Carrier (T # l) by ;
T . v in {w} by ;
then A34: T . v = w by TARSKI:def 1;
A35: Carrier (T # l) c= X by VECTSP_6:def 4;
T | (Carrier (T # l)) is one-to-one by ;
then (T @* (T # l)) . w = (T # l) . v by
.= 0. R by A1, A30, A33, A34, A35, Th42 ;
hence contradiction by A31; :: thesis: verum
end;
hence (T @* (T # l)) . w = l . w by A29; :: thesis: verum
end;
end;