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 FUNCT_2:def 8 :: 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 A2, FUNCT_1:def 6;
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 TARSKI:def 3, VECTSP_6:def 4;
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 A9, FUNCT_2:38;
A13: (T | X) . x = T . x by A10, FUNCT_1:49
.= T . v by A5, A12, TARSKI:def 1
.= (T | X) . v by A4, FUNCT_1:49 ;
A14: x in dom (T | X) by A10, A11, RELAT_1:57;
v in dom (T | X) by A3, A4, RELAT_1:57;
then x = v by A1, A13, A14, FUNCT_1:def 4;
then x in {v} by TARSKI:def 1;
hence x in {v} /\ (Carrier (T # l)) by A9, XBOOLE_0:def 4; :: 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 A5, A16, TARSKI:def 1;
then x in T " {w} by FUNCT_2:38;
hence x in (T " {w}) /\ (Carrier (T # l)) by A15, XBOOLE_0:def 4; :: 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 A19, XBOOLE_0:def 4;
x in Carrier (T # l) by A19, XBOOLE_0:def 4;
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 RLVECT_1:43, b1;
A22: (T # l) . v = 0. R by A18;
A23: not v in dom ((X `) --> (0. R)) by A4, XBOOLE_0:def 5;
T # l = (l * T) +* ((X `) --> (0. R)) by A1, Def6;
then (T # l) . v = (l * T) . v by A23, FUNCT_4:11;
hence (T @* (T # l)) . w = l . w by A3, A5, A21, A22, FUNCT_1:13; :: thesis: verum

end;

suppose v in Carrier (T # l) ; :: thesis: (T @* (T # l)) . w = l . w

then (T " {w}) /\ (Carrier (T # l)) = {v} by A17, XBOOLE_1:28, ZFMISC_1:31;
then A24: canFS ((T " {w}) /\ (Carrier (T # l))) = <*v*> by FINSEQ_1:94;
A25: not v in dom ((X `) --> (0. R)) by A4, XBOOLE_0:def 5;
A26: T # l = (l * T) +* ((X `) --> (0. R)) by A1, Def6;
A27: v in dom (T # l) by A7, FUNCT_2:def 1;
A28: v in dom (l * T) by A7, FUNCT_2:def 1;
(T # l) * <*v*> = <*((T # l) . v)*> by A27, FINSEQ_2:34
.= <*((l * T) . v)*> by A25, A26, FUNCT_4:11
.= (l * T) * <*v*> by A28, FINSEQ_2:34
.= l * (T * <*v*>) by RELAT_1:36
.= l * <*(T . v)*> by A3, FINSEQ_2:34
.= <*(l . w)*> by A5, A6, FINSEQ_2:34 ;
then Sum (lCFST ((T # l),T,w)) = l . w by A24, RLVECT_1:44;
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 RANKNULL:3, Th36;
T . v in {w} by A32, FUNCT_1:def 7;
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 A1, RANKNULL:2, VECTSP_6:def 4;
then (T @* (T # l)) . w = (T # l) . v by A33, A34, Th37
.= 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;