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 ;

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 )
;

end;

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)) )

end;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

then A17:
(T " {w}) /\ (Carrier (T # l)) = {v} /\ (Carrier (T # l))
by TARSKI:2;
let x be object ; :: thesis: ( x in (T " {w}) /\ (Carrier (T # l)) iff x in {v} /\ (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;hereby :: thesis: ( x in {v} /\ (Carrier (T # l)) implies x in (T " {w}) /\ (Carrier (T # l)) )

assume
x in {v} /\ (Carrier (T # l))
; :: thesis: 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;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

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

per cases
( not v in Carrier (T # l) or v in Carrier (T # l) )
;

end;

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

{v} /\ (Carrier (T # l)) = {}

(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;proof

then b1:
lCFST ((T # l),T,w) = <*> the carrier of R
by A17;
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 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

(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

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;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

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

then A30:
l . w = 0. R
;

end;now :: thesis: not (T @* (T # l)) . w <> 0. R

hence
(T @* (T # l)) . w = l . w
by A29; :: thesis: verumassume 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;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