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

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

end;

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 A2, FUNCT_1:def 6;

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 A4, FUNCT_1:59 ;

A12: (T @ (T # l)) . w = Sum ((T # l) .: (T " {(T . v)})) by A7, Def5

.= Sum ({(l . (T . v))} \/ ((T # l) .: B)) by A9, A10, A11, RELAT_1:120 ;

end;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 A2, FUNCT_1:def 6;

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 A4, FUNCT_1:59 ;

A12: (T @ (T # l)) . w = Sum ((T # l) .: (T " {(T . v)})) by A7, Def5

.= Sum ({(l . (T . v))} \/ ((T # l) .: B)) by A9, A10, A11, RELAT_1:120 ;

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

end;

suppose
B = {}
; :: thesis: (T @ (T # l)) . w = l . w

then (T @ (T # l)) . w =
Sum ({(l . (T . v))} \/ ({} F))
by A12

.= l . w by A7, RLVECT_2:9 ;

hence (T @ (T # l)) . w = l . w ; :: thesis: verum

end;.= l . w by A7, RLVECT_2:9 ;

hence (T @ (T # l)) . w = l . w ; :: thesis: verum

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 A8, XBOOLE_1:63;

then (T @ (T # l)) . w = Sum ({(l . (T . v))} \/ {(0. F)}) by A12, A13, Th35

.= (Sum {(l . (T . v))}) + (Sum {(0. F)}) by A3, A7, RLVECT_2:12, ZFMISC_1:11

.= (l . (T . v)) + (Sum {(0. F)}) by RLVECT_2:9

.= (l . (T . v)) + (0. F) by RLVECT_2:9

.= l . w by A7, RLVECT_1:4 ;

hence (T @ (T # l)) . w = l . w ; :: thesis: verum

end;then B misses Carrier (T # l) by A8, XBOOLE_1:63;

then (T @ (T # l)) . w = Sum ({(l . (T . v))} \/ {(0. F)}) by A12, A13, Th35

.= (Sum {(l . (T . v))}) + (Sum {(0. F)}) by A3, A7, RLVECT_2:12, ZFMISC_1:11

.= (l . (T . v)) + (Sum {(0. F)}) by RLVECT_2:9

.= (l . (T . v)) + (0. F) by RLVECT_2:9

.= l . w by A7, RLVECT_1:4 ;

hence (T @ (T # l)) . w = l . w ; :: thesis: verum

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

then A15:
l . w = 0. F
;

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

hence
(T @ (T # l)) . w = l . w
by A14; :: thesis: verumassume 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 A17, FUNCT_1:def 7;

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 A1, Th2;

then (T @ (T # l)) . w = (T # l) . v by A18, A19, Th37

.= 0. F by A1, A15, A18, A19, A20, Th42 ;

hence contradiction by A16; :: thesis: verum

end;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 A17, FUNCT_1:def 7;

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 A1, Th2;

then (T @ (T # l)) . w = (T # l) . v by A18, A19, Th37

.= 0. F by A1, A15, A18, A19, A20, Th42 ;

hence contradiction by A16; :: thesis: verum