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

for T being linear-transformation of V,W

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 holds

T . (Sum l) = Sum Tl

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

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 holds

T . (Sum l) = Sum Tl

let T be linear-transformation of V,W; :: thesis: 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 holds

T . (Sum l) = Sum Tl

A1: T is additive ;

A2: dom T = the carrier of V by FUNCT_2:def 1;

defpred S_{1}[ 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_{1}[ 0 ]
_{1}[n] holds

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

let A be Subset of V; :: thesis: for l being Linear_Combination of A

for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l holds

T . (Sum l) = Sum Tl

let l be Linear_Combination of A; :: thesis: for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l holds

T . (Sum l) = Sum Tl

let Tl be Linear_Combination of T .: (Carrier l); :: thesis: ( Tl = T @* l implies T . (Sum l) = Sum Tl )

assume A104: Tl = T @* l ; :: thesis: T . (Sum l) = Sum Tl

card (T .: (Carrier l)) is Nat ;

hence T . (Sum l) = Sum Tl by A103, A104; :: thesis: verum

for T being linear-transformation of V,W

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 holds

T . (Sum l) = Sum Tl

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

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 holds

T . (Sum l) = Sum Tl

let T be linear-transformation of V,W; :: thesis: 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 holds

T . (Sum l) = Sum Tl

A1: T is additive ;

A2: dom T = the carrier of V by FUNCT_2:def 1;

defpred S

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

proof

A6:
for n being Nat st S
let A be Subset of V; :: thesis: for l being Linear_Combination of A

for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l & card (T .: (Carrier l)) = 0 holds

T . (Sum l) = Sum Tl

let l be Linear_Combination of A; :: thesis: for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l & card (T .: (Carrier l)) = 0 holds

T . (Sum l) = Sum Tl

let Tl be Linear_Combination of T .: (Carrier l); :: thesis: ( Tl = T @* l & card (T .: (Carrier l)) = 0 implies T . (Sum l) = Sum Tl )

assume P1: ( Tl = T @* l & card (T .: (Carrier l)) = 0 ) ; :: thesis: T . (Sum l) = Sum Tl

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

end;for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l & card (T .: (Carrier l)) = 0 holds

T . (Sum l) = Sum Tl

let l be Linear_Combination of A; :: thesis: for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l & card (T .: (Carrier l)) = 0 holds

T . (Sum l) = Sum Tl

let Tl be Linear_Combination of T .: (Carrier l); :: thesis: ( Tl = T @* l & card (T .: (Carrier l)) = 0 implies T . (Sum l) = Sum Tl )

assume P1: ( Tl = T @* l & card (T .: (Carrier l)) = 0 ) ; :: thesis: T . (Sum l) = Sum Tl

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

S

proof

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

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

let A be Subset of V; :: thesis: for l being Linear_Combination of A

for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l & card (T .: (Carrier l)) = n + 1 holds

T . (Sum l) = Sum Tl

let l be Linear_Combination of A; :: thesis: for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l & card (T .: (Carrier l)) = n + 1 holds

T . (Sum l) = Sum Tl

let Tl be Linear_Combination of T .: (Carrier l); :: thesis: ( Tl = T @* l & card (T .: (Carrier l)) = n + 1 implies T . (Sum l) = Sum Tl )

assume A7: ( Tl = T @* l & card (T .: (Carrier l)) = n + 1 ) ; :: thesis: T . (Sum l) = Sum Tl

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_{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;

A27: 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;

A31: l1 | (Carrier l1) = l | (Carrier 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)) = {}

A50: for w being Vector of W st w in T .: (Carrier l0) holds

Tl . w = Tl0 . w

Tl . w = Tl1 . w

x in Carrier Tl

x in Carrier Tl

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}

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}

A88: T . (Sum l1) = Sum 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: verum

end;assume A21: S

let A be Subset of V; :: thesis: for l being Linear_Combination of A

for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l & card (T .: (Carrier l)) = n + 1 holds

T . (Sum l) = Sum Tl

let l be Linear_Combination of A; :: thesis: for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l & card (T .: (Carrier l)) = n + 1 holds

T . (Sum l) = Sum Tl

let Tl be Linear_Combination of T .: (Carrier l); :: thesis: ( Tl = T @* l & card (T .: (Carrier l)) = n + 1 implies T . (Sum l) = Sum Tl )

assume A7: ( Tl = T @* l & card (T .: (Carrier l)) = n + 1 ) ; :: thesis: T . (Sum l) = Sum Tl

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

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

end;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: 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 . x 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 . x 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 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_{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;

A27: for x being object holds

( x in B0 iff x in Carrier l1 )

proof

then A30:
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 X1;

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

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

assume X1:
x in Carrier l1
; :: thesis: x in B0assume A28:
x in B0
; :: thesis: x in Carrier l1

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

end;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: verum

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

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

A31: l1 | (Carrier l1) = l | (Carrier l1)

proof

A33:
for v being Element of V holds l . v = (l0 + l1) . v
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;

end;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: for x being object st x in Carrier l1 holds

L00 . x = L11 . x

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

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

assume A32: x in Carrier l1 ; :: thesis: L00 . x = L11 . x

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

end;assume A32: x in Carrier l1 ; :: thesis: L00 . x = L11 . x

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

proof

then A42:
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 A34:
not v in Carrier l
; :: thesis: l . v = (l0 + l1) . v

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

end;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: verum

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

end;

per cases
( v in T " {w} or not v in T " {w} )
;

end;

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

A49:
T .: (Carrier l) c= T .: ((Carrier l1) \/ (Carrier l0))
by A42, RELAT_1:123, VECTSP_6:23;
assume
(T .: (Carrier l0)) /\ (T .: (Carrier l1)) <> {}
; :: thesis: contradiction

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

end;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: verum

A50: for w being Vector of W st w in T .: (Carrier l0) holds

Tl . w = Tl0 . w

proof

A58:
for w being Vector of W st w in T .: (Carrier l1) holds
let v be Vector of W; :: thesis: ( v in T .: (Carrier l0) implies Tl . v = Tl0 . v )

assume v in T .: (Carrier l0) ; :: thesis: Tl . v = Tl0 . v

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;

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

end;assume v in T .: (Carrier l0) ; :: thesis: Tl . v = Tl0 . v

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: for s being object st s in (T " {v}) /\ (Carrier l) holds

s in (T " {v}) /\ (Carrier l0)

then
(T " {v}) /\ (Carrier l) c= (T " {v}) /\ (Carrier l0)
;s in (T " {v}) /\ (Carrier l0)

let s be object ; :: thesis: ( s in (T " {v}) /\ (Carrier l) implies s in (T " {v}) /\ (Carrier l0) )

assume s in (T " {v}) /\ (Carrier l) ; :: thesis: s in (T " {v}) /\ (Carrier l0)

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}

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

end;assume s in (T " {v}) /\ (Carrier l) ; :: thesis: s in (T " {v}) /\ (Carrier l0)

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

then
s in Carrier l0
by A19, A55, XBOOLE_0:def 5;
assume
s in T " {w}
; :: thesis: contradiction

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

end;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: verum

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

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

Tl . w = Tl1 . w

proof

A67:
for x being object st x in Carrier Tl0 holds
let v be Vector of W; :: thesis: ( v in T .: (Carrier l1) implies Tl . v = Tl1 . v )

assume v in T .: (Carrier l1) ; :: thesis: Tl . v = Tl1 . v

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;

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

end;assume v in T .: (Carrier l1) ; :: thesis: Tl . v = Tl1 . v

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: for s being object st s in (T " {v}) /\ (Carrier l) holds

s in (T " {v}) /\ (Carrier l1)

then
(T " {v}) /\ (Carrier l) c= (T " {v}) /\ (Carrier l1)
;s in (T " {v}) /\ (Carrier l1)

let s be object ; :: thesis: ( s in (T " {v}) /\ (Carrier l) implies s in (T " {v}) /\ (Carrier l1) )

assume A63: s in (T " {v}) /\ (Carrier l) ; :: thesis: s in (T " {v}) /\ (Carrier l1)

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

end;assume A63: s in (T " {v}) /\ (Carrier l) ; :: thesis: s in (T " {v}) /\ (Carrier l1)

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

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

x in Carrier Tl

proof

A70:
for x being object st x in Carrier Tl1 holds
let x be object ; :: thesis: ( x in Carrier Tl0 implies x in Carrier Tl )

assume A68: x in Carrier Tl0 ; :: thesis: x in Carrier Tl

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

end;assume A68: x in Carrier Tl0 ; :: thesis: x in Carrier Tl

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

x in Carrier Tl

proof

A73:
T .: (Carrier l0) = T .: ((Carrier l) \ (T " {w}))
by A15, TARSKI:2;
let x be object ; :: thesis: ( x in Carrier Tl1 implies x in Carrier Tl )

assume A71: x in Carrier Tl1 ; :: thesis: x in Carrier Tl

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

end;assume A71: x in Carrier Tl1 ; :: thesis: x in Carrier Tl

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

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

then
T .: (Carrier l0) c= (T .: (Carrier l)) \ {w}
;
let x be object ; :: thesis: ( x in T .: (Carrier l0) implies x in (T .: (Carrier l)) \ {w} )

assume x in T .: (Carrier l0) ; :: thesis: x in (T .: (Carrier l)) \ {w}

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}

end;assume x in T .: (Carrier l0) ; :: thesis: x in (T .: (Carrier l)) \ {w}

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

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

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

end;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: verum

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

then A87:
Carrier Tl1 c= {w}
;
let y be object ; :: thesis: ( y in Carrier Tl1 implies y in {w} )

assume A81: y in Carrier Tl1 ; :: thesis: y in {w}

then reconsider v = y as Vector of W ;

A83: Tl1 . v = Sum (lCFST (l1,T,v)) by LDef5;

y = w

end;assume A81: y in Carrier Tl1 ; :: thesis: y in {w}

then reconsider v = y as Vector of W ;

A83: Tl1 . v = Sum (lCFST (l1,T,v)) by LDef5;

y = w

proof

hence
y in {w}
by TARSKI:def 1; :: thesis: verum
assume A84:
y <> w
; :: thesis: contradiction

A85: (T " {v}) /\ (T " {w}) = {}

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

end;A85: (T " {v}) /\ (T " {w}) = {}

proof

set g = canFS ((T " {v}) /\ (Carrier l1));
assume
(T " {v}) /\ (T " {w}) <> {}
; :: thesis: contradiction

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

end;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: verum

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

A88: T . (Sum l1) = Sum Tl1

proof

for w being Element of W holds Tl . w = (Tl0 + Tl1) . w
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

end;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: ( v in Carrier l1 implies T . v = w )

assume v in Carrier l1 ; :: thesis: T . v = w

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

end;assume v in Carrier l1 ; :: thesis: T . v = w

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

per cases
( Sum (lCFST (l1,T,w)) = 0. K or Sum (lCFST (l1,T,w)) <> 0. K )
;

end;

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

then A92:
not w in Carrier Tl1
by A89, VECTSP_6:2;

A93: Carrier Tl1 = {}

.= 0. W by VECTSP_1:14 ;

hence T . (Sum l1) = Sum Tl1 by A93, VECTSP_6:19; :: thesis: verum

end;A93: Carrier Tl1 = {}

proof

T . (Sum l1) =
(0. K) * w
by A90, A91, ThTF3B2
assume
Carrier Tl1 <> {}
; :: thesis: contradiction

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

end;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: verum

.= 0. W by VECTSP_1:14 ;

hence T . (Sum l1) = Sum Tl1 by A93, VECTSP_6:19; :: thesis: verum

proof

then A102:
Tl = Tl0 + Tl1
;
let w be Element of W; :: thesis: Tl . w = (Tl0 + Tl1) . w

end;per cases
( not w in Carrier Tl or w in Carrier Tl )
;

end;

suppose A96:
not w in Carrier Tl
; :: thesis: Tl . w = (Tl0 + Tl1) . w

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

end;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: verum

suppose
w in Carrier Tl
; :: thesis: Tl . w = (Tl0 + Tl1) . w

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

end;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: verum

proof
end;

per cases
( w in T .: (Carrier l1) or w in T .: (Carrier l0) )
by A99, XBOOLE_0:def 3;

end;

suppose A100:
w in T .: (Carrier l1)
; :: thesis: Tl . w = (Tl0 + Tl1) . w

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

end;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: verum

suppose A101:
w in T .: (Carrier l0)
; :: thesis: Tl . w = (Tl0 + Tl1) . w

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

end;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: verum

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

let A be Subset of V; :: thesis: for l being Linear_Combination of A

for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l holds

T . (Sum l) = Sum Tl

let l be Linear_Combination of A; :: thesis: for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l holds

T . (Sum l) = Sum Tl

let Tl be Linear_Combination of T .: (Carrier l); :: thesis: ( Tl = T @* l implies T . (Sum l) = Sum Tl )

assume A104: Tl = T @* l ; :: thesis: T . (Sum l) = Sum Tl

card (T .: (Carrier l)) is Nat ;

hence T . (Sum l) = Sum Tl by A103, A104; :: thesis: verum