let K be Ring; :: thesis: for V, W being LeftMod of K

for T being linear-transformation of V,W

for s being Vector of W

for A being Subset of V

for l being Linear_Combination of A st ( for v being Vector of V st v in Carrier l holds

T . v = s ) holds

T . (Sum l) = (Sum (lCFST (l,T,s))) * s

let V, W be LeftMod of K; :: thesis: for T being linear-transformation of V,W

for s being Vector of W

for A being Subset of V

for l being Linear_Combination of A st ( for v being Vector of V st v in Carrier l holds

T . v = s ) holds

T . (Sum l) = (Sum (lCFST (l,T,s))) * s

let T be linear-transformation of V,W; :: thesis: for s being Vector of W

for A being Subset of V

for l being Linear_Combination of A st ( for v being Vector of V st v in Carrier l holds

T . v = s ) holds

T . (Sum l) = (Sum (lCFST (l,T,s))) * s

let s be Vector of W; :: thesis: for A being Subset of V

for l being Linear_Combination of A st ( for v being Vector of V st v in Carrier l holds

T . v = s ) holds

T . (Sum l) = (Sum (lCFST (l,T,s))) * s

A1: T is additive ;

defpred S_{1}[ Nat] means for A being Subset of V

for l being Linear_Combination of A st card (Carrier l) = $1 & ( for v being Vector of V st v in Carrier l holds

T . v = s ) holds

T . (Sum l) = (Sum (lCFST (l,T,s))) * s;

reconsider SZ0 = {(0. K)} as finite Subset of K ;

A2: S_{1}[ 0 ]
_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A2, A5);

let A be Subset of V; :: thesis: for l being Linear_Combination of A st ( for v being Vector of V st v in Carrier l holds

T . v = s ) holds

T . (Sum l) = (Sum (lCFST (l,T,s))) * s

let l be Linear_Combination of A; :: thesis: ( ( for v being Vector of V st v in Carrier l holds

T . v = s ) implies T . (Sum l) = (Sum (lCFST (l,T,s))) * s )

assume A54: for v being Vector of V st v in Carrier l holds

T . v = s ; :: thesis: T . (Sum l) = (Sum (lCFST (l,T,s))) * s

card (Carrier l) is Nat ;

hence T . (Sum l) = (Sum (lCFST (l,T,s))) * s by A53, A54; :: thesis: verum

for T being linear-transformation of V,W

for s being Vector of W

for A being Subset of V

for l being Linear_Combination of A st ( for v being Vector of V st v in Carrier l holds

T . v = s ) holds

T . (Sum l) = (Sum (lCFST (l,T,s))) * s

let V, W be LeftMod of K; :: thesis: for T being linear-transformation of V,W

for s being Vector of W

for A being Subset of V

for l being Linear_Combination of A st ( for v being Vector of V st v in Carrier l holds

T . v = s ) holds

T . (Sum l) = (Sum (lCFST (l,T,s))) * s

let T be linear-transformation of V,W; :: thesis: for s being Vector of W

for A being Subset of V

for l being Linear_Combination of A st ( for v being Vector of V st v in Carrier l holds

T . v = s ) holds

T . (Sum l) = (Sum (lCFST (l,T,s))) * s

let s be Vector of W; :: thesis: for A being Subset of V

for l being Linear_Combination of A st ( for v being Vector of V st v in Carrier l holds

T . v = s ) holds

T . (Sum l) = (Sum (lCFST (l,T,s))) * s

A1: T is additive ;

defpred S

for l being Linear_Combination of A st card (Carrier l) = $1 & ( for v being Vector of V st v in Carrier l holds

T . v = s ) holds

T . (Sum l) = (Sum (lCFST (l,T,s))) * s;

reconsider SZ0 = {(0. K)} as finite Subset of K ;

A2: S

proof

A5:
for n being Nat st S
let A be Subset of V; :: thesis: for l being Linear_Combination of A st card (Carrier l) = 0 & ( for v being Vector of V st v in Carrier l holds

T . v = s ) holds

T . (Sum l) = (Sum (lCFST (l,T,s))) * s

let l be Linear_Combination of A; :: thesis: ( card (Carrier l) = 0 & ( for v being Vector of V st v in Carrier l holds

T . v = s ) implies T . (Sum l) = (Sum (lCFST (l,T,s))) * s )

assume ( card (Carrier l) = 0 & ( for v being Vector of V st v in Carrier l holds

T . v = s ) ) ; :: thesis: T . (Sum l) = (Sum (lCFST (l,T,s))) * s

then A3: Carrier l = {} ;

then A4: T . (Sum l) = T . (0. V) by VECTSP_6:19

.= T . ((0. K) * (0. V)) by VECTSP_1:14

.= (0. K) * (T . (0. V)) by MOD_2:def 2

.= 0. W by VECTSP_1:14 ;

set g = canFS ((T " {s}) /\ (Carrier l));

lCFST (l,T,s) = <*> the carrier of K by A3;

then Sum (lCFST (l,T,s)) = 0. K by RLVECT_1:43;

hence T . (Sum l) = (Sum (lCFST (l,T,s))) * s by A4, VECTSP_1:14; :: thesis: verum

end;T . v = s ) holds

T . (Sum l) = (Sum (lCFST (l,T,s))) * s

let l be Linear_Combination of A; :: thesis: ( card (Carrier l) = 0 & ( for v being Vector of V st v in Carrier l holds

T . v = s ) implies T . (Sum l) = (Sum (lCFST (l,T,s))) * s )

assume ( card (Carrier l) = 0 & ( for v being Vector of V st v in Carrier l holds

T . v = s ) ) ; :: thesis: T . (Sum l) = (Sum (lCFST (l,T,s))) * s

then A3: Carrier l = {} ;

then A4: T . (Sum l) = T . (0. V) by VECTSP_6:19

.= T . ((0. K) * (0. V)) by VECTSP_1:14

.= (0. K) * (T . (0. V)) by MOD_2:def 2

.= 0. W by VECTSP_1:14 ;

set g = canFS ((T " {s}) /\ (Carrier l));

lCFST (l,T,s) = <*> the carrier of K by A3;

then Sum (lCFST (l,T,s)) = 0. K by RLVECT_1:43;

hence T . (Sum l) = (Sum (lCFST (l,T,s))) * s by A4, VECTSP_1:14; :: thesis: verum

S

proof

A53:
for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A6: S_{1}[n]
; :: thesis: S_{1}[n + 1]

let A be Subset of V; :: thesis: for l being Linear_Combination of A st card (Carrier l) = n + 1 & ( for v being Vector of V st v in Carrier l holds

T . v = s ) holds

T . (Sum l) = (Sum (lCFST (l,T,s))) * s

let l be Linear_Combination of A; :: thesis: ( card (Carrier l) = n + 1 & ( for v being Vector of V st v in Carrier l holds

T . v = s ) implies T . (Sum l) = (Sum (lCFST (l,T,s))) * s )

assume A7: ( card (Carrier l) = n + 1 & ( for v being Vector of V st v in Carrier l holds

T . v = s ) ) ; :: thesis: T . (Sum l) = (Sum (lCFST (l,T,s))) * s

then Carrier l <> {} ;

then consider w being object such that

A8: w in Carrier l by XBOOLE_0:def 1;

reconsider w = w as Element of the carrier of V by A8;

A9: card ((Carrier l) \ {w}) = (card (Carrier l)) - (card {w}) by A8, CARD_2:44, ZFMISC_1:31

.= (n + 1) - 1 by A7, CARD_2:42

.= n ;

reconsider A0 = (Carrier l) \ {w} as finite Subset of V ;

reconsider B0 = {w} as finite Subset of V ;

defpred S_{2}[ object , object ] means ( not $1 is Vector of V or ( $1 in A0 & $2 = l . $1 ) or ( not $1 in A0 & $2 = 0. K ) );

A10: for x being object st x in the carrier of V holds

ex y being object st

( y in the carrier of K & S_{2}[x,y] )

A13: for x being object st x in the carrier of V holds

S_{2}[x,l0 . x]
from FUNCT_2:sch 1(A10);

A14: for v being Vector of V st not v in A0 holds

l0 . v = 0. K by A13;

reconsider l0 = l0 as Element of Funcs ( the carrier of V, the carrier of K) by FUNCT_2:8;

reconsider l0 = l0 as Linear_Combination of V by A14, VECTSP_6:def 1;

A15: for x being object holds

( x in A0 iff x in Carrier l0 )

then reconsider l0 = l0 as Linear_Combination of A0 by VECTSP_6:def 4;

A20: l0 | (Carrier l0) = l | (Carrier l0)_{3}[ object , object ] means ( not $1 is Vector of V or ( $1 in B0 & $2 = l . $1 ) or ( not $1 in B0 & $2 = 0. K ) );

A22: for x being object st x in the carrier of V holds

ex y being object st

( y in the carrier of K & S_{3}[x,y] )

A25: for x being object st x in the carrier of V holds

S_{3}[x,l1 . x]
from FUNCT_2:sch 1(A22);

A26: for v being Vector of V st not v in B0 holds

l1 . v = 0. K by A25;

reconsider l1 = l1 as Element of Funcs ( the carrier of V, the carrier of K) by FUNCT_2:8;

reconsider l1 = l1 as Linear_Combination of V by A26, VECTSP_6:def 1;

for x being object holds

( x in B0 iff x in Carrier l1 )

then reconsider l1 = l1 as Linear_Combination of B0 by VECTSP_6:def 4;

for v being Element of V holds l . v = (l0 + l1) . v

then A39: Sum l = (Sum l0) + (Sum l1) by VECTSP_6:44;

for v being Vector of V st v in Carrier l0 holds

T . v = s

A41: A0 \/ B0 = (Carrier l) \/ B0 by XBOOLE_1:39

.= Carrier l by A8, XBOOLE_1:12, ZFMISC_1:31 ;

A42: w in B0 by TARSKI:def 1;

A43: T . (Sum l1) = T . ((l1 . w) * w) by VECTSP_6:17

.= (l1 . w) * (T . w) by MOD_2:def 2

.= (l1 . w) * s by A7, A8

.= (l . w) * s by A25, A42

.= (Sum <*(l . w)*>) * s by RLVECT_1:44 ;

set WW = (lCFST (l0,T,s)) ^ <*(l /. w)*>;

rng ((lCFST (l0,T,s)) ^ <*(l /. w)*>) = (rng (lCFST (l0,T,s))) \/ (rng <*(l /. w)*>) by FINSEQ_1:31;

then reconsider WW = (lCFST (l0,T,s)) ^ <*(l /. w)*> as FinSequence of K by FINSEQ_1:def 4;

reconsider L = Sum WW as Element of K ;

A44: (T " {s}) /\ (Carrier l) = ((T " {s}) /\ A0) \/ ((T " {s}) /\ B0) by A41, XBOOLE_1:23

.= ((T " {s}) /\ (Carrier l0)) \/ ((T " {s}) /\ B0) by A15, TARSKI:2 ;

reconsider S1 = (T " {s}) /\ (Carrier l0) as finite Subset of V ;

then A47: (T " {s}) /\ B0 = {w} by XBOOLE_1:28;

reconsider S2 = (T " {s}) /\ B0 as finite Subset of the carrier of V ;

A48: ((Carrier l) \ {w}) /\ B0 = (B0 /\ (Carrier l)) \ B0 by XBOOLE_1:49

.= {} by XBOOLE_1:17, XBOOLE_1:37 ;

A49: S1 /\ S2 = (((T " {s}) /\ (Carrier l0)) /\ B0) /\ (T " {s}) by XBOOLE_1:16

.= (((T " {s}) /\ ((Carrier l) \ {w})) /\ B0) /\ (T " {s}) by A15, TARSKI:2

.= ((T " {s}) /\ {}) /\ (T " {s}) by A48, XBOOLE_1:16

.= {} ;

A50: Carrier l0 c= Carrier l by A19, XBOOLE_1:36;

reconsider ll = l as Function of the carrier of V, the carrier of K ;

A51: l * (canFS S2) = ll * <*w*> by A47, FINSEQ_1:94

.= <*(ll . w)*> by FINSEQ_2:35 ;

rng (l * (canFS S1)) c= the carrier of K ;

then reconsider l1 = l * (canFS S1) as FinSequence of K by FINSEQ_1:def 4;

reconsider l2 = l * (canFS S2) as FinSequence of K by A51;

rng (lCFST (l,T,s)) c= the carrier of K ;

then reconsider ll0 = lCFST (l,T,s) as FinSequence of K by FINSEQ_1:def 4;

A52: Sum ll0 = (Sum l1) + (Sum l2) by A44, A49, ThTF3C2

.= (Sum (lCFST (l0,T,s))) + (Sum <*(l . w)*>) by A20, A50, A51, ThTF3C3, XBOOLE_1:17 ;

thus T . (Sum l) = ((Sum (lCFST (l0,T,s))) * s) + ((Sum <*(l . w)*>) * s) by A1, A39, A40, A43

.= (Sum (lCFST (l,T,s))) * s by A52, VECTSP_1:def 15 ; :: thesis: verum

end;assume A6: S

let A be Subset of V; :: thesis: for l being Linear_Combination of A st card (Carrier l) = n + 1 & ( for v being Vector of V st v in Carrier l holds

T . v = s ) holds

T . (Sum l) = (Sum (lCFST (l,T,s))) * s

let l be Linear_Combination of A; :: thesis: ( card (Carrier l) = n + 1 & ( for v being Vector of V st v in Carrier l holds

T . v = s ) implies T . (Sum l) = (Sum (lCFST (l,T,s))) * s )

assume A7: ( card (Carrier l) = n + 1 & ( for v being Vector of V st v in Carrier l holds

T . v = s ) ) ; :: thesis: T . (Sum l) = (Sum (lCFST (l,T,s))) * s

then Carrier l <> {} ;

then consider w being object such that

A8: w in Carrier l by XBOOLE_0:def 1;

reconsider w = w as Element of the carrier of V by A8;

A9: card ((Carrier l) \ {w}) = (card (Carrier l)) - (card {w}) by A8, CARD_2:44, ZFMISC_1:31

.= (n + 1) - 1 by A7, CARD_2:42

.= n ;

reconsider A0 = (Carrier l) \ {w} as finite Subset of V ;

reconsider B0 = {w} as finite Subset of V ;

defpred S

A10: for x being object st x in the carrier of V holds

ex y being object st

( y in the carrier of K & S

proof

consider l0 being Function of the carrier of V, the carrier of K such that
let x be object ; :: thesis: ( x in the carrier of V implies ex y being object st

( y in the carrier of K & S_{2}[x,y] ) )

assume x in the carrier of V ; :: thesis: ex y being object st

( y in the carrier of K & S_{2}[x,y] )

then reconsider x9 = x as Vector of V ;

end;( y in the carrier of K & S

assume x in the carrier of V ; :: thesis: ex y being object st

( y in the carrier of K & S

then reconsider x9 = x as Vector of V ;

per cases
( x in A0 or not x in A0 )
;

end;

suppose A11:
x in A0
; :: thesis: ex y being object st

( y in the carrier of K & S_{2}[x,y] )

( y in the carrier of K & S

l . x9 in the carrier of K
;

hence ex y being object st

( y in the carrier of K & S_{2}[x,y] )
by A11; :: thesis: verum

end;hence ex y being object st

( y in the carrier of K & S

A13: for x being object st x in the carrier of V holds

S

A14: for v being Vector of V st not v in A0 holds

l0 . v = 0. K by A13;

reconsider l0 = l0 as Element of Funcs ( the carrier of V, the carrier of K) by FUNCT_2:8;

reconsider l0 = l0 as Linear_Combination of V by A14, VECTSP_6:def 1;

A15: for x being object holds

( x in A0 iff x in Carrier l0 )

proof

then A19:
Carrier l0 = A0
by TARSKI:2;
let x be object ; :: thesis: ( x in A0 iff x in Carrier l0 )

then reconsider v = x as Vector of V ;

ex v9 being Vector of V st

( v9 = v & l0 . v9 <> 0. K ) by A18;

hence x in A0 by A13; :: thesis: verum

end;hereby :: thesis: ( x in Carrier l0 implies x in A0 )

assume A18:
x in Carrier l0
; :: thesis: x in A0assume A16:
x in A0
; :: thesis: x in Carrier l0

then reconsider v = x as Vector of V ;

A17: l0 . v = l . v by A13, A16;

v in Carrier l by A16, XBOOLE_0:def 5;

then l0 . v <> 0. K by A17, VECTSP_6:2;

hence x in Carrier l0 ; :: thesis: verum

end;then reconsider v = x as Vector of V ;

A17: l0 . v = l . v by A13, A16;

v in Carrier l by A16, XBOOLE_0:def 5;

then l0 . v <> 0. K by A17, VECTSP_6:2;

hence x in Carrier l0 ; :: thesis: verum

then reconsider v = x as Vector of V ;

ex v9 being Vector of V st

( v9 = v & l0 . v9 <> 0. K ) by A18;

hence x in A0 by A13; :: thesis: verum

then reconsider l0 = l0 as Linear_Combination of A0 by VECTSP_6:def 4;

A20: l0 | (Carrier l0) = l | (Carrier l0)

proof

defpred S
reconsider L0 = l0 as Function of V,K ;

reconsider L1 = l as Function of V,K ;

reconsider L00 = L0 | (Carrier l0) as Function of (Carrier l0), the carrier of K by FUNCT_2:32;

reconsider L11 = L1 | (Carrier l0) as Function of (Carrier l0), the carrier of K by FUNCT_2:32;

end;reconsider L1 = l as Function of V,K ;

reconsider L00 = L0 | (Carrier l0) as Function of (Carrier l0), the carrier of K by FUNCT_2:32;

reconsider L11 = L1 | (Carrier l0) as Function of (Carrier l0), the carrier of K by FUNCT_2:32;

now :: thesis: for x being object st x in Carrier l0 holds

L00 . x = L11 . x

hence
l0 | (Carrier l0) = l | (Carrier l0)
by FUNCT_2:12; :: thesis: verumL00 . x = L11 . x

let x be object ; :: thesis: ( x in Carrier l0 implies L00 . x = L11 . x )

assume A21: x in Carrier l0 ; :: thesis: L00 . x = L11 . x

then reconsider v = x as Vector of V ;

thus L00 . x = l0 . v by A21, FUNCT_1:49

.= l . v by A13, A19, A21

.= L11 . x by A21, FUNCT_1:49 ; :: thesis: verum

end;assume A21: x in Carrier l0 ; :: thesis: L00 . x = L11 . x

then reconsider v = x as Vector of V ;

thus L00 . x = l0 . v by A21, FUNCT_1:49

.= l . v by A13, A19, A21

.= L11 . x by A21, FUNCT_1:49 ; :: thesis: verum

A22: for x being object st x in the carrier of V holds

ex y being object st

( y in the carrier of K & S

proof

consider l1 being Function of V,K such that
let x be object ; :: thesis: ( x in the carrier of V implies ex y being object st

( y in the carrier of K & S_{3}[x,y] ) )

assume x in the carrier of V ; :: thesis: ex y being object st

( y in the carrier of K & S_{3}[x,y] )

then reconsider x9 = x as Vector of V ;

end;( y in the carrier of K & S

assume x in the carrier of V ; :: thesis: ex y being object st

( y in the carrier of K & S

then reconsider x9 = x as Vector of V ;

per cases
( x in B0 or not x in B0 )
;

end;

suppose A23:
x in B0
; :: thesis: ex y being object st

( y in the carrier of K & S_{3}[x,y] )

( y in the carrier of K & S

l . x9 in the carrier of K
;

hence ex y being object st

( y in the carrier of K & S_{3}[x,y] )
by A23; :: thesis: verum

end;hence ex y being object st

( y in the carrier of K & S

A25: for x being object st x in the carrier of V holds

S

A26: for v being Vector of V st not v in B0 holds

l1 . v = 0. K by A25;

reconsider l1 = l1 as Element of Funcs ( the carrier of V, the carrier of K) by FUNCT_2:8;

reconsider l1 = l1 as Linear_Combination of V by A26, VECTSP_6:def 1;

for x being object holds

( x in B0 iff x in Carrier l1 )

proof

then
Carrier l1 = B0
by TARSKI:2;
let x be object ; :: thesis: ( x in B0 iff x in Carrier l1 )

then reconsider v = x as Vector of V ;

ex v9 being Vector of V st

( v9 = v & l1 . v9 <> 0. K ) by A30;

hence x in B0 by A25; :: thesis: verum

end;hereby :: thesis: ( x in Carrier l1 implies x in B0 )

assume A30:
x in Carrier l1
; :: thesis: x in B0assume A27:
x in B0
; :: thesis: x in Carrier l1

then A28: x = w by TARSKI:def 1;

then A29: l1 . w = l . w by A25, A27;

l . w <> 0. K by A8, VECTSP_6:2;

hence x in Carrier l1 by A28, A29; :: thesis: verum

end;then A28: x = w by TARSKI:def 1;

then A29: l1 . w = l . w by A25, A27;

l . w <> 0. K by A8, VECTSP_6:2;

hence x in Carrier l1 by A28, A29; :: thesis: verum

then reconsider v = x as Vector of V ;

ex v9 being Vector of V st

( v9 = v & l1 . v9 <> 0. K ) by A30;

hence x in B0 by A25; :: thesis: verum

then reconsider l1 = l1 as Linear_Combination of B0 by VECTSP_6:def 4;

for v being Element of V holds l . v = (l0 + l1) . v

proof

then
l = l0 + l1
;
let v be Element of V; :: thesis: l . v = (l0 + l1) . v

end;per cases
( not v in Carrier l or v in Carrier l )
;

end;

suppose A31:
not v in Carrier l
; :: thesis: l . v = (l0 + l1) . v

then A32:
l . v = 0. K
;

not v in A0 by A31, XBOOLE_0:def 5;

then l0 . v = 0. K by A13;

then l . v = (l0 . v) + (l1 . v) by A25, A32;

hence l . v = (l0 + l1) . v by VECTSP_6:22; :: thesis: verum

end;not v in A0 by A31, XBOOLE_0:def 5;

then l0 . v = 0. K by A13;

then l . v = (l0 . v) + (l1 . v) by A25, A32;

hence l . v = (l0 + l1) . v by VECTSP_6:22; :: thesis: verum

suppose A34:
v in Carrier l
; :: thesis: l . v = (l0 + l1) . v

end;

then A39: Sum l = (Sum l0) + (Sum l1) by VECTSP_6:44;

for v being Vector of V st v in Carrier l0 holds

T . v = s

proof

then A40:
T . (Sum l0) = (Sum (lCFST (l0,T,s))) * s
by A6, A9, A19;
let v be Vector of V; :: thesis: ( v in Carrier l0 implies T . v = s )

assume v in Carrier l0 ; :: thesis: T . v = s

then v in Carrier l by A19, XBOOLE_0:def 5;

hence T . v = s by A7; :: thesis: verum

end;assume v in Carrier l0 ; :: thesis: T . v = s

then v in Carrier l by A19, XBOOLE_0:def 5;

hence T . v = s by A7; :: thesis: verum

A41: A0 \/ B0 = (Carrier l) \/ B0 by XBOOLE_1:39

.= Carrier l by A8, XBOOLE_1:12, ZFMISC_1:31 ;

A42: w in B0 by TARSKI:def 1;

A43: T . (Sum l1) = T . ((l1 . w) * w) by VECTSP_6:17

.= (l1 . w) * (T . w) by MOD_2:def 2

.= (l1 . w) * s by A7, A8

.= (l . w) * s by A25, A42

.= (Sum <*(l . w)*>) * s by RLVECT_1:44 ;

set WW = (lCFST (l0,T,s)) ^ <*(l /. w)*>;

rng ((lCFST (l0,T,s)) ^ <*(l /. w)*>) = (rng (lCFST (l0,T,s))) \/ (rng <*(l /. w)*>) by FINSEQ_1:31;

then reconsider WW = (lCFST (l0,T,s)) ^ <*(l /. w)*> as FinSequence of K by FINSEQ_1:def 4;

reconsider L = Sum WW as Element of K ;

A44: (T " {s}) /\ (Carrier l) = ((T " {s}) /\ A0) \/ ((T " {s}) /\ B0) by A41, XBOOLE_1:23

.= ((T " {s}) /\ (Carrier l0)) \/ ((T " {s}) /\ B0) by A15, TARSKI:2 ;

reconsider S1 = (T " {s}) /\ (Carrier l0) as finite Subset of V ;

now :: thesis: for z being object st z in B0 holds

z in T " {s}

then
B0 c= T " {s}
;z in T " {s}

let z be object ; :: thesis: ( z in B0 implies z in T " {s} )

assume A45: z in B0 ; :: thesis: z in T " {s}

T . w = s by A7, A8;

then A46: T . w in {s} by TARSKI:def 1;

w in T " {s} by A46, FUNCT_2:38;

hence z in T " {s} by A45, TARSKI:def 1; :: thesis: verum

end;assume A45: z in B0 ; :: thesis: z in T " {s}

T . w = s by A7, A8;

then A46: T . w in {s} by TARSKI:def 1;

w in T " {s} by A46, FUNCT_2:38;

hence z in T " {s} by A45, TARSKI:def 1; :: thesis: verum

then A47: (T " {s}) /\ B0 = {w} by XBOOLE_1:28;

reconsider S2 = (T " {s}) /\ B0 as finite Subset of the carrier of V ;

A48: ((Carrier l) \ {w}) /\ B0 = (B0 /\ (Carrier l)) \ B0 by XBOOLE_1:49

.= {} by XBOOLE_1:17, XBOOLE_1:37 ;

A49: S1 /\ S2 = (((T " {s}) /\ (Carrier l0)) /\ B0) /\ (T " {s}) by XBOOLE_1:16

.= (((T " {s}) /\ ((Carrier l) \ {w})) /\ B0) /\ (T " {s}) by A15, TARSKI:2

.= ((T " {s}) /\ {}) /\ (T " {s}) by A48, XBOOLE_1:16

.= {} ;

A50: Carrier l0 c= Carrier l by A19, XBOOLE_1:36;

reconsider ll = l as Function of the carrier of V, the carrier of K ;

A51: l * (canFS S2) = ll * <*w*> by A47, FINSEQ_1:94

.= <*(ll . w)*> by FINSEQ_2:35 ;

rng (l * (canFS S1)) c= the carrier of K ;

then reconsider l1 = l * (canFS S1) as FinSequence of K by FINSEQ_1:def 4;

reconsider l2 = l * (canFS S2) as FinSequence of K by A51;

rng (lCFST (l,T,s)) c= the carrier of K ;

then reconsider ll0 = lCFST (l,T,s) as FinSequence of K by FINSEQ_1:def 4;

A52: Sum ll0 = (Sum l1) + (Sum l2) by A44, A49, ThTF3C2

.= (Sum (lCFST (l0,T,s))) + (Sum <*(l . w)*>) by A20, A50, A51, ThTF3C3, XBOOLE_1:17 ;

thus T . (Sum l) = ((Sum (lCFST (l0,T,s))) * s) + ((Sum <*(l . w)*>) * s) by A1, A39, A40, A43

.= (Sum (lCFST (l,T,s))) * s by A52, VECTSP_1:def 15 ; :: thesis: verum

let A be Subset of V; :: thesis: for l being Linear_Combination of A st ( for v being Vector of V st v in Carrier l holds

T . v = s ) holds

T . (Sum l) = (Sum (lCFST (l,T,s))) * s

let l be Linear_Combination of A; :: thesis: ( ( for v being Vector of V st v in Carrier l holds

T . v = s ) implies T . (Sum l) = (Sum (lCFST (l,T,s))) * s )

assume A54: for v being Vector of V st v in Carrier l holds

T . v = s ; :: thesis: T . (Sum l) = (Sum (lCFST (l,T,s))) * s

card (Carrier l) is Nat ;

hence T . (Sum l) = (Sum (lCFST (l,T,s))) * s by A53, A54; :: thesis: verum