let K be Ring; :: thesis:
let V, W be LeftMod of K; :: thesis:
let T be linear-transformation of V,W; :: thesis:
let s be Vector of W; :: thesis:
A1: T is additive ;
defpred S₁[ 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₁[ 0 ]

let A be Subset of V; :: thesis:
let l be Linear_Combination of A; :: thesis:
assume ( card (Carrier l) = 0 & ( for v being Vector of V st v in Carrier l holds
T . v = s ) ) ; :: thesis:
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:

end;

A5: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A6: S₁[n] ; :: thesis:
let A be Subset of V; :: thesis:
let l be Linear_Combination of A; :: thesis:
assume A7: ( card (Carrier l) = n + 1 & ( for v being Vector of V st v in Carrier l holds
T . v = s ) ) ; :: thesis:
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₂[ 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₂[x,y] )

proof

let x be object ; :: thesis:
assume x in the carrier of V ; :: thesis:
then reconsider x9 = x as Vector of V ;

per cases ;

suppose A11: x in A0 ; :: thesis:

l . x9 in the carrier of K ;
hence ex y being object st
( y in the carrier of K & S₂[x,y] ) by A11; :: thesis:

end;

suppose not x in A0 ; :: thesis:

hence ex y being object st
( y in the carrier of K & S₂[x,y] ) ; :: thesis:

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
S₂[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 )

proof

let x be object ; :: thesis:

hereby :: thesis:

assume A16: x in A0 ; :: thesis:
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:

end;

assume A18: x in Carrier l0 ; :: thesis:
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:

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:

let x be object ; :: thesis:
assume A21: x in Carrier l0 ; :: thesis:
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:

end;

hence l0 | (Carrier l0) = l | (Carrier l0) by FUNCT_2:12; :: thesis:

end;

defpred S₃[ 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₃[x,y] )

proof

let x be object ; :: thesis:
assume x in the carrier of V ; :: thesis:
then reconsider x9 = x as Vector of V ;

per cases ;

suppose A23: x in B0 ; :: thesis:

l . x9 in the carrier of K ;
hence ex y being object st
( y in the carrier of K & S₃[x,y] ) by A23; :: thesis:

end;

suppose not x in B0 ; :: thesis:

hence ex y being object st
( y in the carrier of K & S₃[x,y] ) ; :: thesis:

end;

consider l1 being Function of V,K such that
A25: for x being object st x in the carrier of V holds
S₃[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 )

proof

let x be object ; :: thesis:

hereby :: thesis:

assume A27: x in B0 ; :: thesis:
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:

end;

assume A30: x in Carrier l1 ; :: thesis:
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:

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:

per cases ;

suppose A31: not v in Carrier l ; :: thesis:

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:

end;

suppose A34: v in Carrier l ; :: thesis:

per cases ;

suppose A35: v in {w} ; :: thesis:

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 A25, A35;
hence l . v = (l0 + l1) . v by VECTSP_6:22; :: thesis:

end;

suppose A37: not v in {w} ; :: thesis:

then A38: v in A0 by A34, XBOOLE_0:def 5;
l1 . v = 0. K by A25, A37;
then l . v = (l0 . v) + (l1 . v) by A13, A38;
hence l . v = (l0 + l1) . v by VECTSP_6:22; :: thesis:

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:
assume v in Carrier l0 ; :: thesis:
then v in Carrier l by A19, XBOOLE_0:def 5;
hence T . v = s by A7; :: thesis:

end;

then A40: T . (Sum l0) = (Sum (lCFST (l0,T,s))) * s by A6, A9, A19;
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:

let z be object ; :: thesis:
assume A45: z in B0 ; :: thesis:
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:

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: ((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:

end;

A53: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A5);
let A be Subset of V; :: thesis:
let l be Linear_Combination of A; :: thesis:
assume A54: for v being Vector of V st v in Carrier l holds
T . v = s ; :: thesis:
card (Carrier l) is Nat ;
hence T . (Sum l) = (Sum (lCFST (l,T,s))) * s by A53, A54; :: thesis: