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

defpred S1[ Nat] means for A being Subset of V
for l being Linear_Combination of A st card () = \$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: S1[ 0 ]
proof
let A be Subset of V; :: thesis: for l being Linear_Combination of A st card () = 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 () = 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 () = 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}) /\ ());
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 ; :: thesis: verum
end;
A5: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A6: S1[n] ; :: thesis: S1[n + 1]
let A be Subset of V; :: thesis: for l being Linear_Combination of A st card () = 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 () = 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 () = 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 (() \ {w}) = (card ()) - () by
.= (n + 1) - 1 by
.= n ;
reconsider A0 = () \ {w} as finite Subset of V ;
reconsider B0 = {w} as finite Subset of V ;
defpred S2[ 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 & S2[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier of V implies ex y being object st
( y in the carrier of K & S2[x,y] ) )

assume x in the carrier of V ; :: thesis: ex y being object st
( y in the carrier of K & S2[x,y] )

then reconsider x9 = x as Vector of V ;
per cases ( x in A0 or not x in A0 ) ;
suppose A11: x in A0 ; :: thesis: ex y being object st
( y in the carrier of K & S2[x,y] )

l . x9 in the carrier of K ;
hence ex y being object st
( y in the carrier of K & S2[x,y] ) by A11; :: thesis: verum
end;
suppose not x in A0 ; :: thesis: ex y being object st
( y in the carrier of K & S2[x,y] )

hence ex y being object st
( y in the carrier of K & S2[x,y] ) ; :: thesis: verum
end;
end;
end;
consider l0 being Function of the carrier of V, the carrier of K such that
A13: for x being object st x in the carrier of V holds
S2[x,l0 . x] from 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 ;
A15: for x being object holds
( x in A0 iff x in Carrier l0 )
proof
let x be object ; :: thesis: ( x in A0 iff x in Carrier l0 )
hereby :: thesis: ( x in Carrier l0 implies x in A0 )
assume A16: x in A0 ; :: thesis: x in Carrier l0
then reconsider v = x as Vector of V ;
A17: l0 . v = l . v by ;
v in Carrier l by ;
then l0 . v <> 0. K by ;
hence x in Carrier l0 ; :: thesis: verum
end;
assume A18: x in Carrier l0 ; :: thesis: x in A0
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;
then A19: Carrier l0 = A0 by TARSKI:2;
then reconsider l0 = l0 as Linear_Combination of A0 by VECTSP_6:def 4;
A20: l0 | (Carrier l0) = l | (Carrier l0)
proof
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;
now :: thesis: for x being object st x in Carrier l0 holds
L00 . 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
.= l . v by
.= L11 . x by ; :: thesis: verum
end;
hence l0 | (Carrier l0) = l | (Carrier l0) by FUNCT_2:12; :: thesis: verum
end;
defpred S3[ 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 & S3[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier of V implies ex y being object st
( y in the carrier of K & S3[x,y] ) )

assume x in the carrier of V ; :: thesis: ex y being object st
( y in the carrier of K & S3[x,y] )

then reconsider x9 = x as Vector of V ;
per cases ( x in B0 or not x in B0 ) ;
suppose A23: x in B0 ; :: thesis: ex y being object st
( y in the carrier of K & S3[x,y] )

l . x9 in the carrier of K ;
hence ex y being object st
( y in the carrier of K & S3[x,y] ) by A23; :: thesis: verum
end;
suppose not x in B0 ; :: thesis: ex y being object st
( y in the carrier of K & S3[x,y] )

hence ex y being object st
( y in the carrier of K & S3[x,y] ) ; :: thesis: verum
end;
end;
end;
consider l1 being Function of V,K such that
A25: for x being object st x in the carrier of V holds
S3[x,l1 . x] from 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 ;
for x being object holds
( x in B0 iff x in Carrier l1 )
proof
let x be object ; :: thesis: ( x in B0 iff x in Carrier l1 )
hereby :: thesis: ( x in Carrier l1 implies x in B0 )
assume A27: x in B0 ; :: thesis: x in Carrier l1
then A28: x = w by TARSKI:def 1;
then A29: l1 . w = l . w by ;
l . w <> 0. K by ;
hence x in Carrier l1 by ; :: thesis: verum
end;
assume A30: x in Carrier l1 ; :: thesis: x in B0
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;
then Carrier l1 = B0 by TARSKI:2;
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
let v be Element of V; :: thesis: l . v = (l0 + l1) . v
per cases ;
suppose A31: not v in Carrier l ; :: thesis: l . v = (l0 + l1) . v
then A32: l . v = 0. K ;
not v in A0 by ;
then l0 . v = 0. K by A13;
then l . v = (l0 . v) + (l1 . v) by ;
hence l . v = (l0 + l1) . v by VECTSP_6:22; :: thesis: verum
end;
suppose A34: v in Carrier l ; :: thesis: l . v = (l0 + l1) . v
per cases ( v in {w} or not v in {w} ) ;
suppose A35: v in {w} ; :: thesis: l . v = (l0 + l1) . v
then not v in A0 by XBOOLE_0:def 5;
then l0 . v = 0. K by A13;
then l . v = (l0 . v) + (l1 . v) by ;
hence l . v = (l0 + l1) . v by VECTSP_6:22; :: thesis: verum
end;
suppose A37: not v in {w} ; :: thesis: l . v = (l0 + l1) . v
then A38: v in A0 by ;
l1 . v = 0. K by ;
then l . v = (l0 . v) + (l1 . v) by ;
hence l . v = (l0 + l1) . v by VECTSP_6:22; :: thesis: verum
end;
end;
end;
end;
end;
then l = l0 + l1 ;
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
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 ;
hence T . v = s by A7; :: thesis: verum
end;
then A40: T . (Sum l0) = (Sum (lCFST (l0,T,s))) * s by A6, A9, A19;
A41: A0 \/ B0 = () \/ B0 by XBOOLE_1:39
.= Carrier l by ;
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
.= (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}) /\ () = ((T " {s}) /\ A0) \/ ((T " {s}) /\ B0) by
.= ((T " {s}) /\ (Carrier l0)) \/ ((T " {s}) /\ B0) by ;
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}
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 ;
hence z in T " {s} by ; :: thesis: verum
end;
then B0 c= T " {s} ;
then A47: (T " {s}) /\ B0 = {w} by XBOOLE_1:28;
reconsider S2 = (T " {s}) /\ B0 as finite Subset of the carrier of V ;
A48: (() \ {w}) /\ B0 = (B0 /\ ()) \ B0 by XBOOLE_1:49
.= {} by ;
A49: S1 /\ S2 = (((T " {s}) /\ (Carrier l0)) /\ B0) /\ (T " {s}) by XBOOLE_1:16
.= (((T " {s}) /\ (() \ {w})) /\ B0) /\ (T " {s}) by
.= ((T " {s}) /\ {}) /\ (T " {s}) by
.= {} ;
A50: Carrier l0 c= Carrier l by ;
reconsider ll = l as Function of the carrier of V, the carrier of K ;
A51: l * (canFS S2) = ll * <*w*> by
.= <*(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
.= (Sum (lCFST (l0,T,s))) + (Sum <*(l . w)*>) by ;
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 ; :: thesis: verum
end;
A53: for n being Nat holds S1[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 () is Nat ;
hence T . (Sum l) = (Sum (lCFST (l,T,s))) * s by ; :: thesis: verum