let K be Ring; :: thesis:
let V, W be LeftMod of K; :: thesis:
let T be linear-transformation of V,W; :: thesis:
A1: T is additive ;
A2: dom T = the carrier of V by FUNCT_2:def 1;
defpred S₁[ Nat] means for A being Subset of V
for l being Linear_Combination of A
for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l & card (T .: (Carrier l)) = $1 holds
T . (Sum l) = Sum Tl;
A3: S₁[ 0 ]

let A be Subset of V; :: thesis:
let l be Linear_Combination of A; :: thesis:
let Tl be Linear_Combination of T .: (Carrier l); :: thesis:
assume P1: ( Tl = T @* l & card (T .: (Carrier l)) = 0 ) ; :: thesis:
A4: T .: (Carrier l) = {} by P1;
( Carrier l = {} or not Carrier l c= dom T ) by P1;
then A5: T . (Sum l) = T . (0. V) by A2, 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 ;
Carrier (T @* l) c= {} by A4, LDef5;
then Carrier (T @* l) = {} ;
hence T . (Sum l) = Sum Tl by A5, P1, VECTSP_6:19; :: thesis:

end;

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

proof

let n be Nat; :: thesis:
assume A21: S₁[n] ; :: thesis:
let A be Subset of V; :: thesis:
let l be Linear_Combination of A; :: thesis:
let Tl be Linear_Combination of T .: (Carrier l); :: thesis:
assume A7: ( Tl = T @* l & card (T .: (Carrier l)) = n + 1 ) ; :: thesis:
then T .: (Carrier l) <> {} ;
then consider w being object such that
A8: w in T .: (Carrier l) by XBOOLE_0:def 1;
reconsider w = w as Element of the carrier of W by A8;
A9: card ((T .: (Carrier l)) \ {w}) = (card (T .: (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) \ (T " {w}) as finite Subset of V ;
reconsider B0 = (T " {w}) /\ (Carrier l) as Subset of V ;
reconsider B0 = B0 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

set L0 = l0;
set L1 = l;
reconsider L00 = l0 | (Carrier l0) as Function of (Carrier l0), the carrier of K by FUNCT_2:32;
reconsider L11 = l | (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 . x 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 the carrier of V, the carrier of 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;
A27: for x being object holds
( x in B0 iff x in Carrier l1 )

proof

let x be object ; :: thesis:

hereby :: thesis:

assume A28: x in B0 ; :: thesis:
then reconsider v = x as Vector of V ;
A29: l1 . v = l . v by A25, A28;
v in Carrier l by A28, XBOOLE_0:def 4;
then l1 . v <> 0. K by A29, VECTSP_6:2;
hence x in Carrier l1 ; :: thesis:

end;

assume X1: 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 X1;
hence x in B0 by A25; :: thesis:

end;

then A30: Carrier l1 = B0 by TARSKI:2;
then reconsider l1 = l1 as Linear_Combination of B0 by VECTSP_6:def 4;
A31: l1 | (Carrier l1) = l | (Carrier l1)

proof

reconsider L0 = l1 as Function of V,K ;
reconsider L1 = l as Function of V,K ;
reconsider L00 = L0 | (Carrier l1) as Function of (Carrier l1), the carrier of K by FUNCT_2:32;
reconsider L11 = L1 | (Carrier l1) as Function of (Carrier l1), the carrier of K by FUNCT_2:32;

now :: thesis:

let x be object ; :: thesis:
assume A32: x in Carrier l1 ; :: thesis:
then reconsider v = x as Vector of V ;
thus L00 . x = L0 . x by A32, FUNCT_1:49
.= l . v by A25, A30, A32
.= L11 . x by A32, FUNCT_1:49 ; :: thesis:

end;

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

end;

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

proof

let v be Element of V; :: thesis:

per cases ;

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

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

end;

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

per cases ;

suppose A38: v in T " {w} ; :: thesis:

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

end;

suppose A40: not v in T " {w} ; :: thesis:

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

end;

then A42: l = l0 + l1 ;
reconsider Tl0 = T @* l0 as Linear_Combination of T .: (Carrier l0) by LTh29;
reconsider Tl1 = T @* l1 as Linear_Combination of T .: (Carrier l1) by LTh29;
A43: (T .: (Carrier l0)) /\ (T .: (Carrier l1)) = {}

proof

assume (T .: (Carrier l0)) /\ (T .: (Carrier l1)) <> {} ; :: thesis:
then consider y being object such that
A44: y in (T .: (Carrier l0)) /\ (T .: (Carrier l1)) by XBOOLE_0:def 1;
A45: ( y in T .: (Carrier l0) & y in T .: (Carrier l1) ) by A44, XBOOLE_0:def 4;
then consider x being object such that
A46: ( x in the carrier of V & x in Carrier l0 & y = T . x ) by FUNCT_2:64;
consider z being object such that
A47: ( z in the carrier of V & z in Carrier l1 & y = T . z ) by A45, FUNCT_2:64;
x in (Carrier l) \ (T " {w}) by A15, A46;
then not x in T " {w} by XBOOLE_0:def 5;
then A48: not y in {w} by A46, FUNCT_2:38;
z in (T " {w}) /\ (Carrier l) by A27, A47;
then z in T " {w} by XBOOLE_0:def 4;
hence contradiction by A47, A48, FUNCT_2:38; :: thesis:

end;

A49: T .: (Carrier l) c= T .: ((Carrier l1) \/ (Carrier l0)) by A42, RELAT_1:123, VECTSP_6:23;
A50: for w being Vector of W st w in T .: (Carrier l0) holds
Tl . w = Tl0 . w

proof

let v be Vector of W; :: thesis:
assume v in T .: (Carrier l0) ; :: thesis:
then consider x being object such that
A51: ( x in the carrier of V & x in Carrier l0 & v = T . x ) by FUNCT_2:64;
reconsider x = x as Vector of V by A51;
A52: Tl0 . v = Sum (lCFST (l0,T,v)) by LDef5;
A53: Tl . v = Sum (lCFST (l,T,v)) by A7, LDef5;
A54: Carrier l0 c= Carrier l by A19, XBOOLE_1:36;

now :: thesis:

let s be object ; :: thesis:
assume s in (T " {v}) /\ (Carrier l) ; :: thesis:
then A55: ( s in T " {v} & s in Carrier l ) by XBOOLE_0:def 4;
then ( s in the carrier of V & T . s in {v} ) by FUNCT_2:38;
then A56: T . s = T . x by A51, TARSKI:def 1;
not s in T " {w}

proof

assume s in T " {w} ; :: thesis:
then T . x in {w} by A56, FUNCT_2:38;
then x in T " {w} by FUNCT_2:38;
hence contradiction by A19, A51, XBOOLE_0:def 5; :: thesis:

end;

then s in Carrier l0 by A19, A55, XBOOLE_0:def 5;
hence s in (T " {v}) /\ (Carrier l0) by A55, XBOOLE_0:def 4; :: thesis:

end;

then (T " {v}) /\ (Carrier l) c= (T " {v}) /\ (Carrier l0) ;
then A57: (T " {v}) /\ (Carrier l0) = (T " {v}) /\ (Carrier l) by A19, XBOOLE_1:26, XBOOLE_1:36;
reconsider XX = (T " {v}) /\ (Carrier l0) as finite Subset of V ;
thus Tl . v = Tl0 . v by A20, A52, A53, A54, A57, ThTF3C3, XBOOLE_1:17; :: thesis:

end;

A58: for w being Vector of W st w in T .: (Carrier l1) holds
Tl . w = Tl1 . w

proof

let v be Vector of W; :: thesis:
assume v in T .: (Carrier l1) ; :: thesis:
then consider x being object such that
A59: ( x in the carrier of V & x in Carrier l1 & v = T . x ) by FUNCT_2:64;
reconsider x = x as Vector of V by A59;
A60: Tl1 . v = Sum (lCFST (l1,T,v)) by LDef5;
A61: Tl . v = Sum (lCFST (l,T,v)) by A7, LDef5;
A62: Carrier l1 c= Carrier l by A30, XBOOLE_1:17;

now :: thesis:

let s be object ; :: thesis:
assume A63: s in (T " {v}) /\ (Carrier l) ; :: thesis:
then A64: ( s in T " {v} & s in Carrier l ) by XBOOLE_0:def 4;
then ( s in the carrier of V & T . s in {v} ) by FUNCT_2:38;
then A65: T . s = T . x by A59, TARSKI:def 1;
x in T " {w} by A30, A59, XBOOLE_0:def 4;
then T . s in {w} by A65, FUNCT_2:38;
then s in T " {w} by A63, FUNCT_2:38;
then s in Carrier l1 by A30, A64, XBOOLE_0:def 4;
hence s in (T " {v}) /\ (Carrier l1) by A64, XBOOLE_0:def 4; :: thesis:

end;

then (T " {v}) /\ (Carrier l) c= (T " {v}) /\ (Carrier l1) ;
then A66: (T " {v}) /\ (Carrier l1) = (T " {v}) /\ (Carrier l) by A30, XBOOLE_1:17, XBOOLE_1:26;
reconsider XX = (T " {v}) /\ (Carrier l1) as finite Subset of V ;
thus Tl . v = Tl1 . v by A31, A60, A61, A62, A66, ThTF3C3, XBOOLE_1:17; :: thesis:

end;

A67: for x being object st x in Carrier Tl0 holds
x in Carrier Tl

proof

let x be object ; :: thesis:
assume A68: x in Carrier Tl0 ; :: thesis:
then reconsider v = x as Vector of W ;
A69: v in T .: (Carrier l0) by A68, LDef5, TARSKI:def 3;
Tl0 . v <> 0. K by A68, VECTSP_6:2;
then Tl . v <> 0. K by A50, A69;
hence x in Carrier Tl ; :: thesis:

end;

A70: for x being object st x in Carrier Tl1 holds
x in Carrier Tl

proof

let x be object ; :: thesis:
assume A71: x in Carrier Tl1 ; :: thesis:
then reconsider v = x as Vector of W ;
A72: v in T .: (Carrier l1) by A71, LDef5, TARSKI:def 3;
Tl1 . v <> 0. K by A71, VECTSP_6:2;
then Tl . v <> 0. K by A58, A72;
hence x in Carrier Tl ; :: thesis:

end;

A73: T .: (Carrier l0) = T .: ((Carrier l) \ (T " {w})) by A15, TARSKI:2;
then A74: (T .: (Carrier l)) \ (T .: (T " {w})) c= T .: (Carrier l0) by RELAT_1:122;
A75: T .: (Carrier l) c= T .: (dom T) by RELAT_1:114;
A76: T .: (Carrier l) c= rng T by A75, RELAT_1:113;
for x being object st x in T .: (Carrier l0) holds
x in (T .: (Carrier l)) \ {w}

proof

let x be object ; :: thesis:
assume x in T .: (Carrier l0) ; :: thesis:
then consider z being object such that
A77: ( z in the carrier of V & z in (Carrier l) \ (T " {w}) & x = T . z ) by A73, FUNCT_2:64;
z in Carrier l by A77, XBOOLE_0:def 5;
then A78: x in T .: (Carrier l) by A77, FUNCT_2:35;
not x in {w}

proof

assume A79: x in {w} ; :: thesis:
z in dom T by A77, FUNCT_2:def 1;
then z in T " {w} by A77, A79, FUNCT_1:def 7;
hence contradiction by A77, XBOOLE_0:def 5; :: thesis:

end;

hence x in (T .: (Carrier l)) \ {w} by A78, XBOOLE_0:def 5; :: thesis:

end;

then T .: (Carrier l0) c= (T .: (Carrier l)) \ {w} ;
then A80: T .: (Carrier l0) = (T .: (Carrier l)) \ {w} by A8, A74, A76, FUNCT_1:77, ZFMISC_1:31;
for y being object st y in Carrier Tl1 holds
y in {w}

proof

let y be object ; :: thesis:
assume A81: y in Carrier Tl1 ; :: thesis:
then reconsider v = y as Vector of W ;
A83: Tl1 . v = Sum (lCFST (l1,T,v)) by LDef5;
y = w

proof

assume A84: y <> w ; :: thesis:
A85: (T " {v}) /\ (T " {w}) = {}

proof

assume (T " {v}) /\ (T " {w}) <> {} ; :: thesis:
then consider x being object such that
A86: x in (T " {v}) /\ (T " {w}) by XBOOLE_0:def 1;
( x in T " {v} & x in T " {w} ) by A86, XBOOLE_0:def 4;
then ( T . x in {v} & T . x in {w} ) by FUNCT_1:def 7;
then ( T . x = v & T . x = w ) by TARSKI:def 1;
hence contradiction by A84; :: thesis:

end;

set g = canFS ((T " {v}) /\ (Carrier l1));
(T " {v}) /\ (Carrier l1) = (T " {v}) /\ ((T " {w}) /\ (Carrier l)) by A27, TARSKI:2
.= {} /\ (Carrier l) by A85, XBOOLE_1:16
.= {} ;
then lCFST (l1,T,v) = <*> the carrier of K ;
hence contradiction by A81, A83, RLVECT_1:43, VECTSP_6:2; :: thesis:

end;

hence y in {w} by TARSKI:def 1; :: thesis:

end;

then A87: Carrier Tl1 c= {w} ;
A88: T . (Sum l1) = Sum Tl1

proof

A89: Tl1 . w = Sum (lCFST (l1,T,w)) by LDef5;
reconsider w = w as Vector of W ;
A90: for v being Vector of V st v in Carrier l1 holds
T . v = w

proof

let v be Vector of V; :: thesis:
assume v in Carrier l1 ; :: thesis:
then v in (T " {w}) /\ (Carrier l) by A27;
then v in T " {w} by XBOOLE_0:def 4;
then T . v in {w} by FUNCT_1:def 7;
hence T . v = w by TARSKI:def 1; :: thesis:

end;

per cases ;

suppose A91: Sum (lCFST (l1,T,w)) = 0. K ; :: thesis:

then A92: not w in Carrier Tl1 by A89, VECTSP_6:2;
A93: Carrier Tl1 = {}

proof

assume Carrier Tl1 <> {} ; :: thesis:
then consider x being object such that
A94: x in Carrier Tl1 by XBOOLE_0:def 1;
thus contradiction by A87, A92, A94, TARSKI:def 1; :: thesis:

end;

T . (Sum l1) = (0. K) * w by A90, A91, ThTF3B2
.= 0. W by VECTSP_1:14 ;
hence T . (Sum l1) = Sum Tl1 by A93, VECTSP_6:19; :: thesis:

end;

suppose Sum (lCFST (l1,T,w)) <> 0. K ; :: thesis:

then w in Carrier Tl1 by A89;
then A95: {w} = Carrier Tl1 by A87, ZFMISC_1:31;
Sum Tl1 = (Sum (lCFST (l1,T,w))) * w by A89, A95, VECTSP_6:20
.= T . (Sum l1) by A90, ThTF3B2 ;
hence T . (Sum l1) = Sum Tl1 ; :: thesis:

end;

for w being Element of W holds Tl . w = (Tl0 + Tl1) . w

proof

let w be Element of W; :: thesis:

per cases ;

suppose A96: not w in Carrier Tl ; :: thesis:

then A97: Tl . w = 0. K ;
not w in Carrier Tl0 by A67, A96;
then A98: Tl0 . w = 0. K ;
not w in Carrier Tl1 by A70, A96;
then Tl . w = (Tl1 . w) + (Tl0 . w) by A97, A98;
hence Tl . w = (Tl0 + Tl1) . w by VECTSP_6:22; :: thesis:

end;

suppose w in Carrier Tl ; :: thesis:

then w in T .: (Carrier l) by TARSKI:def 3, VECTSP_6:def 4;
then w in T .: ((Carrier l0) \/ (Carrier l1)) by A49;
then A99: w in (T .: (Carrier l0)) \/ (T .: (Carrier l1)) by RELAT_1:120;
thus Tl . w = (Tl0 + Tl1) . w :: thesis:

proof

per cases by A99, XBOOLE_0:def 3;

suppose A100: w in T .: (Carrier l1) ; :: thesis:

not w in T .: (Carrier l0) by A43, A100, XBOOLE_0:def 4;
then not w in Carrier Tl0 by LDef5, TARSKI:def 3;
then Tl0 . w = 0. K ;
then Tl . w = (Tl1 . w) + (Tl0 . w) by A58, A100;
hence Tl . w = (Tl0 + Tl1) . w by VECTSP_6:22; :: thesis:

end;

suppose A101: w in T .: (Carrier l0) ; :: thesis:

not w in T .: (Carrier l1) by A43, A101, XBOOLE_0:def 4;
then not w in Carrier Tl1 by LDef5, TARSKI:def 3;
then Tl1 . w = 0. K ;
then Tl . w = (Tl1 . w) + (Tl0 . w) by A50, A101;
hence Tl . w = (Tl0 + Tl1) . w by VECTSP_6:22; :: thesis:

end;

then A102: Tl = Tl0 + Tl1 ;
l = l0 + l1 by A33;
hence T . (Sum l) = T . ((Sum l0) + (Sum l1)) by VECTSP_6:44
.= (T . (Sum l0)) + (T . (Sum l1)) by A1
.= (Sum Tl0) + (Sum Tl1) by A9, A21, A80, A88
.= Sum Tl by A102, VECTSP_6:44 ;
:: thesis:

end;

A103: for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A6);
let A be Subset of V; :: thesis:
let l be Linear_Combination of A; :: thesis:
let Tl be Linear_Combination of T .: (Carrier l); :: thesis:
assume A104: Tl = T @* l ; :: thesis:
card (T .: (Carrier l)) is Nat ;
hence T . (Sum l) = Sum Tl by A103, A104; :: thesis: