:: VECTSP11 semantic presentation

begin


theorem Th1: :: VECTSP11:1
for n, m being Nat
for K being Field
for A, B being Matrix of K
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A holds
Segm ((A + B),nt,mt) = (Segm (A,nt,mt)) + (Segm (B,nt,mt))
proof
let n, m be Nat; ::_thesis: for K being Field
for A, B being Matrix of K
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A holds
Segm ((A + B),nt,mt) = (Segm (A,nt,mt)) + (Segm (B,nt,mt))
let K be Field; ::_thesis: for A, B being Matrix of K
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A holds
Segm ((A + B),nt,mt) = (Segm (A,nt,mt)) + (Segm (B,nt,mt))
let A, B be Matrix of K; ::_thesis: for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A holds
Segm ((A + B),nt,mt) = (Segm (A,nt,mt)) + (Segm (B,nt,mt))
let nt be Element of n -tuples_on NAT; ::_thesis: for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A holds
Segm ((A + B),nt,mt) = (Segm (A,nt,mt)) + (Segm (B,nt,mt))
let mt be Element of m -tuples_on NAT; ::_thesis: ( [:(rng nt),(rng mt):] c= Indices A implies Segm ((A + B),nt,mt) = (Segm (A,nt,mt)) + (Segm (B,nt,mt)) )
assume A1: [:(rng nt),(rng mt):] c= Indices A ; ::_thesis: Segm ((A + B),nt,mt) = (Segm (A,nt,mt)) + (Segm (B,nt,mt))
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_(Segm_((A_+_B),nt,mt))_holds_
(Segm_((A_+_B),nt,mt))_*_(i,j)_=_((Segm_(A,nt,mt))_+_(Segm_(B,nt,mt)))_*_(i,j)
A2: Indices (Segm (A,nt,mt)) = Indices (Segm (B,nt,mt)) by MATRIX_1:26;
let i, j be Nat; ::_thesis: ( [i,j] in Indices (Segm ((A + B),nt,mt)) implies (Segm ((A + B),nt,mt)) * (i,j) = ((Segm (A,nt,mt)) + (Segm (B,nt,mt))) * (i,j) )
assume A3: [i,j] in Indices (Segm ((A + B),nt,mt)) ; ::_thesis: (Segm ((A + B),nt,mt)) * (i,j) = ((Segm (A,nt,mt)) + (Segm (B,nt,mt))) * (i,j)
reconsider nti = nt . i, mtj = mt . j as Nat by VALUED_0:12;
A4: Indices (Segm ((A + B),nt,mt)) = Indices (Segm (A,nt,mt)) by MATRIX_1:26;
then A5: [(nt . i),(mt . j)] in Indices A by A1, A3, MATRIX13:17;
thus (Segm ((A + B),nt,mt)) * (i,j) = (A + B) * (nti,mtj) by A3, MATRIX13:def_1
.= (A * (nti,mtj)) + (B * (nti,mtj)) by A5, MATRIX_3:def_3
.= ((Segm (A,nt,mt)) * (i,j)) + (B * (nti,mtj)) by A3, A4, MATRIX13:def_1
.= ((Segm (A,nt,mt)) * (i,j)) + ((Segm (B,nt,mt)) * (i,j)) by A3, A4, A2, MATRIX13:def_1
.= ((Segm (A,nt,mt)) + (Segm (B,nt,mt))) * (i,j) by A3, A4, MATRIX_3:def_3 ; ::_thesis: verum
end;
hence  Segm ((A + B),nt,mt) = (Segm (A,nt,mt)) + (Segm (B,nt,mt)) by MATRIX_1:27; ::_thesis: verum
end;

theorem Th2: :: VECTSP11:2
for n being Nat
for K being Field
for P being finite without_zero Subset of NAT st P c= Seg n holds
Segm ((1. (K,n)),P,P) = 1. (K,(card P))
proof
let n be Nat; ::_thesis: for K being Field
for P being finite without_zero Subset of NAT st P c= Seg n holds
Segm ((1. (K,n)),P,P) = 1. (K,(card P))
let K be Field; ::_thesis: for P being finite without_zero Subset of NAT st P c= Seg n holds
Segm ((1. (K,n)),P,P) = 1. (K,(card P))
let P be finite without_zero Subset of NAT; ::_thesis: ( P c= Seg n implies Segm ((1. (K,n)),P,P) = 1. (K,(card P)) )
assume A1: P c= Seg n ; ::_thesis: Segm ((1. (K,n)),P,P) = 1. (K,(card P))
set S = Segm ((1. (K,n)),P,P);
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_(1._(K,(card_P)))_holds_
(1._(K,(card_P)))_*_(i,j)_=_(Segm_((1._(K,n)),P,P))_*_(i,j)
set SP = Sgm P;
let i, j be Nat; ::_thesis: ( [i,j] in Indices (1. (K,(card P))) implies (1. (K,(card P))) * (i,j) = (Segm ((1. (K,n)),P,P)) * (i,j) )
assume A2: [i,j] in Indices (1. (K,(card P))) ; ::_thesis: (1. (K,(card P))) * (i,j) = (Segm ((1. (K,n)),P,P)) * (i,j)
A3: Sgm P is one-to-one by A1, FINSEQ_3:92;
A4: rng (Sgm P) = P by A1, FINSEQ_1:def_13;
reconsider Spi = (Sgm P) . i, Spj = (Sgm P) . j as Nat by VALUED_0:12;
A5: Indices (1. (K,(card P))) = Indices (Segm ((1. (K,n)),P,P)) by MATRIX_1:26;
then A6: (Segm ((1. (K,n)),P,P)) * (i,j) = (1. (K,n)) * (Spi,Spj) by A2, MATRIX13:def_1;
 ( Indices (1. (K,n)) = [:(Seg n),(Seg n):] & [:P,P:] c= [:(Seg n),(Seg n):] ) by A1, MATRIX_1:24, ZFMISC_1:96;
then A7: [((Sgm P) . i),((Sgm P) . j)] in Indices (1. (K,n)) by A2, A5, A4, MATRIX13:17;
 ( Indices (Segm ((1. (K,n)),P,P)) = [:(Seg (card P)),(Seg (card P)):] & dom (Sgm P) = Seg (card P) ) by A1, FINSEQ_3:40, MATRIX_1:24;
then A8: ( i in dom (Sgm P) & j in dom (Sgm P) ) by A2, A5, ZFMISC_1:87;
 ( i = j or i <> j ) ;
then  ( ( (Segm ((1. (K,n)),P,P)) * (i,j) = 1_ K & (1. (K,(card P))) * (i,j) = 1_ K ) or ( (1. (K,(card P))) * (i,j) = 0. K & (Sgm P) . i <> (Sgm P) . j ) ) by A2, A3, A7, A8, A6, FUNCT_1:def_4, MATRIX_1:def_11;
hence  (1. (K,(card P))) * (i,j) = (Segm ((1. (K,n)),P,P)) * (i,j) by A7, A6, MATRIX_1:def_11; ::_thesis: verum
end;
hence  Segm ((1. (K,n)),P,P) = 1. (K,(card P)) by MATRIX_1:27; ::_thesis: verum
end;

theorem Th3: :: VECTSP11:3
for K being Field
for A, B being Matrix of K
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices A holds
Segm ((A + B),P,Q) = (Segm (A,P,Q)) + (Segm (B,P,Q))
proof
let K be Field; ::_thesis: for A, B being Matrix of K
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices A holds
Segm ((A + B),P,Q) = (Segm (A,P,Q)) + (Segm (B,P,Q))
let A, B be Matrix of K; ::_thesis: for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices A holds
Segm ((A + B),P,Q) = (Segm (A,P,Q)) + (Segm (B,P,Q))
let P, Q be finite without_zero Subset of NAT; ::_thesis: ( [:P,Q:] c= Indices A implies Segm ((A + B),P,Q) = (Segm (A,P,Q)) + (Segm (B,P,Q)) )
assume A1: [:P,Q:] c= Indices A ; ::_thesis: Segm ((A + B),P,Q) = (Segm (A,P,Q)) + (Segm (B,P,Q))
 ex m being Nat st Q c= Seg m by MATRIX13:43;
then A2: rng (Sgm Q) = Q by FINSEQ_1:def_13;
 ex n being Nat st P c= Seg n by MATRIX13:43;
then  rng (Sgm P) = P by FINSEQ_1:def_13;
hence  Segm ((A + B),P,Q) = (Segm (A,P,Q)) + (Segm (B,P,Q)) by A1, A2, Th1; ::_thesis: verum
end;

theorem Th4: :: VECTSP11:4
for n, i, j being Nat
for K being Field
for A, B being Matrix of n,K st i in Seg n & j in Seg n holds
Delete ((A + B),i,j) = (Delete (A,i,j)) + (Delete (B,i,j))
proof
let n, i, j be Nat; ::_thesis: for K being Field
for A, B being Matrix of n,K st i in Seg n & j in Seg n holds
Delete ((A + B),i,j) = (Delete (A,i,j)) + (Delete (B,i,j))
let K be Field; ::_thesis: for A, B being Matrix of n,K st i in Seg n & j in Seg n holds
Delete ((A + B),i,j) = (Delete (A,i,j)) + (Delete (B,i,j))
let A, B be Matrix of n,K; ::_thesis: ( i in Seg n & j in Seg n implies Delete ((A + B),i,j) = (Delete (A,i,j)) + (Delete (B,i,j)) )
assume A1: ( i in Seg n & j in Seg n ) ; ::_thesis: Delete ((A + B),i,j) = (Delete (A,i,j)) + (Delete (B,i,j))
 ( (Seg n) \ {i} c= Seg n & (Seg n) \ {j} c= Seg n ) by XBOOLE_1:36;
then A2: [:((Seg n) \ {i}),((Seg n) \ {j}):] c= [:(Seg n),(Seg n):] by ZFMISC_1:96;
A3: Indices A = [:(Seg n),(Seg n):] by MATRIX_1:24;
thus  Delete ((A + B),i,j) = Deleting ((A + B),i,j) by A1, LAPLACE:def_1
.= Segm ((A + B),((Seg n) \ {i}),((Seg n) \ {j})) by MATRIX13:58
.= (Segm (A,((Seg n) \ {i}),((Seg n) \ {j}))) + (Segm (B,((Seg n) \ {i}),((Seg n) \ {j}))) by A2, A3, Th3
.= (Deleting (A,i,j)) + (Segm (B,((Seg n) \ {i}),((Seg n) \ {j}))) by MATRIX13:58
.= (Deleting (A,i,j)) + (Deleting (B,i,j)) by MATRIX13:58
.= (Delete (A,i,j)) + (Deleting (B,i,j)) by A1, LAPLACE:def_1
.= (Delete (A,i,j)) + (Delete (B,i,j)) by A1, LAPLACE:def_1 ; ::_thesis: verum
end;

theorem Th5: :: VECTSP11:5
for n, i, j being Nat
for K being Field
for a being Element of K
for A being Matrix of n,K st i in Seg n & j in Seg n holds
Delete ((a * A),i,j) = a * (Delete (A,i,j))
proof
let n, i, j be Nat; ::_thesis: for K being Field
for a being Element of K
for A being Matrix of n,K st i in Seg n & j in Seg n holds
Delete ((a * A),i,j) = a * (Delete (A,i,j))
let K be Field; ::_thesis: for a being Element of K
for A being Matrix of n,K st i in Seg n & j in Seg n holds
Delete ((a * A),i,j) = a * (Delete (A,i,j))
let a be Element of K; ::_thesis: for A being Matrix of n,K st i in Seg n & j in Seg n holds
Delete ((a * A),i,j) = a * (Delete (A,i,j))
let A be Matrix of n,K; ::_thesis: ( i in Seg n & j in Seg n implies Delete ((a * A),i,j) = a * (Delete (A,i,j)) )
assume A1: ( i in Seg n & j in Seg n ) ; ::_thesis: Delete ((a * A),i,j) = a * (Delete (A,i,j))
 ( (Seg n) \ {i} c= Seg n & (Seg n) \ {j} c= Seg n ) by XBOOLE_1:36;
then A2: [:((Seg n) \ {i}),((Seg n) \ {j}):] c= [:(Seg n),(Seg n):] by ZFMISC_1:96;
A3: Indices A = [:(Seg n),(Seg n):] by MATRIX_1:24;
thus  Delete ((a * A),i,j) = Deleting ((a * A),i,j) by A1, LAPLACE:def_1
.= Segm ((a * A),((Seg n) \ {i}),((Seg n) \ {j})) by MATRIX13:58
.= a * (Segm (A,((Seg n) \ {i}),((Seg n) \ {j}))) by A2, A3, MATRIX13:63
.= a * (Deleting (A,i,j)) by MATRIX13:58
.= a * (Delete (A,i,j)) by A1, LAPLACE:def_1 ; ::_thesis: verum
end;

theorem Th6: :: VECTSP11:6
for i, n being Nat
for K being Field st i in Seg n holds
Delete ((1. (K,n)),i,i) = 1. (K,(n -' 1))
proof
let i, n be Nat; ::_thesis: for K being Field st i in Seg n holds
Delete ((1. (K,n)),i,i) = 1. (K,(n -' 1))
let K be Field; ::_thesis: ( i in Seg n implies Delete ((1. (K,n)),i,i) = 1. (K,(n -' 1)) )
assume A1: i in Seg n ; ::_thesis: Delete ((1. (K,n)),i,i) = 1. (K,(n -' 1))
then  n <> 0 ;
then  n >= 1 by NAT_1:14;
then  n -' 1 = n - 1 by XREAL_1:233;
then  card (Seg n) = (n -' 1) + 1 by FINSEQ_1:57;
then A2: card ((Seg n) \ {i}) = n -' 1 by A1, STIRL2_1:55;
thus  Delete ((1. (K,n)),i,i) = Deleting ((1. (K,n)),i,i) by A1, LAPLACE:def_1
.= Segm ((1. (K,n)),((Seg n) \ {i}),((Seg n) \ {i})) by MATRIX13:58
.= 1. (K,(n -' 1)) by A2, Th2, XBOOLE_1:36 ; ::_thesis: verum
end;

theorem Th7: :: VECTSP11:7
for n being Nat
for K being Field
for A, B being Matrix of n,K ex P being Polynomial of K st
( len P <= n + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * B)) ) )
proof
let n be Nat; ::_thesis: for K being Field
for A, B being Matrix of n,K ex P being Polynomial of K st
( len P <= n + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * B)) ) )
let K be Field; ::_thesis: for A, B being Matrix of n,K ex P being Polynomial of K st
( len P <= n + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * B)) ) )
defpred S1[ Nat] means  for A, B being Matrix of $1,K ex P being Polynomial of K st
( len P <= $1 + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * B)) ) );
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
set n1 = n + 1;
let A, B be Matrix of n + 1,K; ::_thesis: ex P being Polynomial of K st
( len P <= (n + 1) + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * B)) ) )
defpred S2[ Nat] means ( $1 <= n + 1 implies ex P being Polynomial of K st
( len P <= (n + 1) + 1 & ( for x being Element of K holds eval (P,x) = Sum ((LaplaceExpL ((A + (x * B)),(n + 1))) | $1) ) ) );
A3: n + 1 in Seg (n + 1) by FINSEQ_1:4;
A4: for m being Nat st S2[m] holds
S2[m + 1]
proof
let m be Nat; ::_thesis: ( S2[m] implies S2[m + 1] )
assume A5: S2[m] ; ::_thesis: S2[m + 1]
set m1 = m + 1;
assume A6: m + 1 <= n + 1 ; ::_thesis: ex P being Polynomial of K st
( len P <= (n + 1) + 1 & ( for x being Element of K holds eval (P,x) = Sum ((LaplaceExpL ((A + (x * B)),(n + 1))) | (m + 1)) ) )
then consider P being Polynomial of K such that
A7: len P <= (n + 1) + 1 and
A8: for x being Element of K holds eval (P,x) = Sum ((LaplaceExpL ((A + (x * B)),(n + 1))) | m) by A5, NAT_1:13;
 1 <= m + 1 by NAT_1:11;
then A9: m + 1 in Seg (n + 1) by A6;
then A10: [(n + 1),(m + 1)] in [:(Seg (n + 1)),(Seg (n + 1)):] by A3, ZFMISC_1:87;
set pow = (power K) . ((- (1_ K)),((m + 1) + (n + 1)));
set DB = Delete (B,(n + 1),(m + 1));
set DA = Delete (A,(n + 1),(m + 1));
set P2 = <%((A * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1))))),((B * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1)))))%>;
A11: Indices B = [:(Seg (n + 1)),(Seg (n + 1)):] by MATRIX_1:24;
 (n + 1) -' 1 = n by NAT_D:34;
then consider P1 being Polynomial of K such that
A12: len P1 <= n + 1 and
A13: for x being Element of K holds eval (P1,x) = Det ((Delete (A,(n + 1),(m + 1))) + (x * (Delete (B,(n + 1),(m + 1))))) by A2;
take PP = P + (P1 *' <%((A * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1))))),((B * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1)))))%>); ::_thesis: ( len PP <= (n + 1) + 1 & ( for x being Element of K holds eval (PP,x) = Sum ((LaplaceExpL ((A + (x * B)),(n + 1))) | (m + 1)) ) )
 len <%((A * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1))))),((B * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1)))))%> <= 2 by POLYNOM5:39;
then  (len P1) + (len <%((A * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1))))),((B * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1)))))%>) <= (n + 1) + 2 by A12, XREAL_1:7;
then A14: ((len P1) + (len <%((A * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1))))),((B * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1)))))%>)) -' 1 <= ((n + 1) + 2) -' 1 by NAT_D:42;
 ( ((n + 2) + 1) -' 1 = n + 2 & len (P1 *' <%((A * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1))))),((B * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1)))))%>) <= ((len P1) + (len <%((A * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1))))),((B * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1)))))%>)) -' 1 ) by HILBASIS:21, NAT_D:34;
then  len (P1 *' <%((A * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1))))),((B * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1)))))%>) <= (n + 1) + 1 by A14, XXREAL_0:2;
hence  len PP <= (n + 1) + 1 by A7, POLYNOM4:6; ::_thesis: for x being Element of K holds eval (PP,x) = Sum ((LaplaceExpL ((A + (x * B)),(n + 1))) | (m + 1))
let x be Element of K; ::_thesis: eval (PP,x) = Sum ((LaplaceExpL ((A + (x * B)),(n + 1))) | (m + 1))
set L = LaplaceExpL ((A + (x * B)),(n + 1));
A15: Indices A = [:(Seg (n + 1)),(Seg (n + 1)):] by MATRIX_1:24;
A16: ((A * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1))))) + (((B * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1))))) * x) = ((A * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1))))) + (((B * ((n + 1),(m + 1))) * x) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1))))) by GROUP_1:def_3
.= ((A * ((n + 1),(m + 1))) + ((B * ((n + 1),(m + 1))) * x)) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1)))) by VECTSP_1:def_2
.= ((A * ((n + 1),(m + 1))) + ((x * B) * ((n + 1),(m + 1)))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1)))) by A10, A11, MATRIX_3:def_5
.= ((A + (x * B)) * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1)))) by A10, A15, MATRIX_3:def_3 ;
 n + 1 = len (LaplaceExpL ((A + (x * B)),(n + 1))) by LAPLACE:def_7;
then A17: dom (LaplaceExpL ((A + (x * B)),(n + 1))) = Seg (n + 1) by FINSEQ_1:def_3;
then A18: (LaplaceExpL ((A + (x * B)),(n + 1))) | (m + 1) = ((LaplaceExpL ((A + (x * B)),(n + 1))) | m) ^ <*((LaplaceExpL ((A + (x * B)),(n + 1))) . (m + 1))*> by A9, FINSEQ_5:10;
A19: (Delete (A,(n + 1),(m + 1))) + (x * (Delete (B,(n + 1),(m + 1)))) = (Delete (A,(n + 1),(m + 1))) + (Delete ((x * B),(n + 1),(m + 1))) by A3, A9, Th5
.= Delete ((A + (x * B)),(n + 1),(m + 1)) by A3, A9, Th4 ;
eval ((P1 *' <%((A * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1))))),((B * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1)))))%>),x) = (eval (P1,x)) * (eval (<%((A * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1))))),((B * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1)))))%>,x)) by POLYNOM4:24
.= (Det ((Delete (A,(n + 1),(m + 1))) + (x * (Delete (B,(n + 1),(m + 1)))))) * (eval (<%((A * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1))))),((B * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1)))))%>,x)) by A13
.= (Minor ((A + (x * B)),(n + 1),(m + 1))) * (((A + (x * B)) * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1))))) by A16, A19, POLYNOM5:44
.= ((A + (x * B)) * ((n + 1),(m + 1))) * (Cofactor ((A + (x * B)),(n + 1),(m + 1))) by GROUP_1:def_3
.= (LaplaceExpL ((A + (x * B)),(n + 1))) . (m + 1) by A9, A17, LAPLACE:def_7 ;
hence  Sum ((LaplaceExpL ((A + (x * B)),(n + 1))) | (m + 1)) = (Sum ((LaplaceExpL ((A + (x * B)),(n + 1))) | m)) + (eval ((P1 *' <%((A * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1))))),((B * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1)))))%>),x)) by A18, FVSUM_1:71
.= (eval (P,x)) + (eval ((P1 *' <%((A * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1))))),((B * ((n + 1),(m + 1))) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1)))))%>),x)) by A8
.= eval (PP,x) by POLYNOM4:19 ;
::_thesis: verum
end;
A20: S2[ 0 ]
proof
assume  0 <= n + 1 ; ::_thesis: ex P being Polynomial of K st
( len P <= (n + 1) + 1 & ( for x being Element of K holds eval (P,x) = Sum ((LaplaceExpL ((A + (x * B)),(n + 1))) | 0) ) )
take P = 0_. K; ::_thesis: ( len P <= (n + 1) + 1 & ( for x being Element of K holds eval (P,x) = Sum ((LaplaceExpL ((A + (x * B)),(n + 1))) | 0) ) )
thus  len P <= (n + 1) + 1 by POLYNOM4:3; ::_thesis: for x being Element of K holds eval (P,x) = Sum ((LaplaceExpL ((A + (x * B)),(n + 1))) | 0)
let x be Element of K; ::_thesis: eval (P,x) = Sum ((LaplaceExpL ((A + (x * B)),(n + 1))) | 0)
 (LaplaceExpL ((A + (x * B)),(n + 1))) | 0 = <*> the carrier of K ;
hence  Sum ((LaplaceExpL ((A + (x * B)),(n + 1))) | 0) = 0. K by RLVECT_1:43
.= eval (P,x) by POLYNOM4:17 ;
::_thesis: verum
end;
 for m being Nat holds S2[m] from NAT_1:sch_2(A20, A4);
then consider P being Polynomial of K such that
A21: len P <= (n + 1) + 1 and
A22: for x being Element of K holds eval (P,x) = Sum ((LaplaceExpL ((A + (x * B)),(n + 1))) | (n + 1)) ;
take  P ; ::_thesis: ( len P <= (n + 1) + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * B)) ) )
thus  len P <= (n + 1) + 1 by A21; ::_thesis: for x being Element of K holds eval (P,x) = Det (A + (x * B))
let x be Element of K; ::_thesis: eval (P,x) = Det (A + (x * B))
A23: len (LaplaceExpL ((A + (x * B)),(n + 1))) = n + 1 by LAPLACE:def_7;
thus  eval (P,x) = Sum ((LaplaceExpL ((A + (x * B)),(n + 1))) | (n + 1)) by A22
.= Sum (LaplaceExpL ((A + (x * B)),(n + 1))) by A23, FINSEQ_1:58
.= Det (A + (x * B)) by A3, LAPLACE:25 ; ::_thesis: verum
end;
A24: S1[ 0 ]
proof
let A, B be Matrix of 0 ,K; ::_thesis: ex P being Polynomial of K st
( len P <= 0 + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * B)) ) )
take P = 1_. K; ::_thesis: ( len P <= 0 + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * B)) ) )
thus  len P <= 0 + 1 by POLYNOM4:4; ::_thesis: for x being Element of K holds eval (P,x) = Det (A + (x * B))
let x be Element of K; ::_thesis: eval (P,x) = Det (A + (x * B))
thus  Det (A + (x * B)) = 1_ K by MATRIXR2:41
.= eval (P,x) by POLYNOM4:18 ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A24, A1);
hence  for A, B being Matrix of n,K ex P being Polynomial of K st
( len P <= n + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * B)) ) ) ; ::_thesis: verum
end;

theorem Th8: :: VECTSP11:8
for n being Nat
for K being Field
for A being Matrix of n,K ex P being Polynomial of K st
( len P = n + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * (1. (K,n)))) ) )
proof
let n be Nat; ::_thesis: for K being Field
for A being Matrix of n,K ex P being Polynomial of K st
( len P = n + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * (1. (K,n)))) ) )
let K be Field; ::_thesis: for A being Matrix of n,K ex P being Polynomial of K st
( len P = n + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * (1. (K,n)))) ) )
defpred S1[ Nat] means  for A being Matrix of $1,K ex P being Polynomial of K st
( len P = $1 + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * (1. (K,$1)))) ) );
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
set n1 = n + 1;
let A be Matrix of n + 1,K; ::_thesis: ex P being Polynomial of K st
( len P = (n + 1) + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * (1. (K,(n + 1))))) ) )
set ONE = 1. (K,(n + 1));
A3: Indices (1. (K,(n + 1))) = Indices A by MATRIX_1:26;
defpred S2[ Nat] means ( 1 <= $1 & $1 <= n + 1 implies ex P being Polynomial of K st
( len P = (n + 1) + 1 & ( for x being Element of K holds eval (P,x) = Sum ((LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) | $1) ) ) );
A4: (n + 1) -' 1 = n by NAT_D:34;
A5: 1 <= n + 1 by NAT_1:11;
then A6: 1 in Seg (n + 1) ;
A7: Indices A = [:(Seg (n + 1)),(Seg (n + 1)):] by MATRIX_1:24;
A8: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A9: S2[k] ; ::_thesis: S2[k + 1]
set k1 = k + 1;
assume that
A10: 1 <= k + 1 and
A11: k + 1 <= n + 1 ; ::_thesis: ex P being Polynomial of K st
( len P = (n + 1) + 1 & ( for x being Element of K holds eval (P,x) = Sum ((LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) | (k + 1)) ) )
set pow = (power K) . ((- (1_ K)),((k + 1) + 1));
set P2 = <%((A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1)))),(((1. (K,(n + 1))) * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1))))%>;
A12: k + 1 in Seg (n + 1) by A10, A11;
then A13: [1,(k + 1)] in Indices A by A7, A6, ZFMISC_1:87;
percases ( k = 0 or k >= 1 ) by NAT_1:14;
supposeA14: k = 0 ; ::_thesis: ex P being Polynomial of K st
( len P = (n + 1) + 1 & ( for x being Element of K holds eval (P,x) = Sum ((LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) | (k + 1)) ) )
then (power K) . ((- (1_ K)),((k + 1) + 1)) = (- (1_ K)) * (- (1_ K)) by GROUP_1:51
.= (1_ K) * (1_ K) by VECTSP_1:10
.= 1_ K by VECTSP_1:def_4 ;
then A15: ((1. (K,(n + 1))) * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1))) = (1_ K) * (1_ K) by A3, A13, A14, MATRIX_1:def_11
.= 1_ K by VECTSP_1:def_4 ;
then A16: ( 2 -' 1 = 2 - 1 & <%((A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1)))),(((1. (K,(n + 1))) * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1))))%> . 1 <> 0. K ) by POLYNOM5:38, XREAL_1:233;
 ((1. (K,(n + 1))) * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1))) <> 0. K by A15;
then A17: len <%((A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1)))),(((1. (K,(n + 1))) * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1))))%> = 2 by POLYNOM5:40;
consider P being Polynomial of K such that
A18: len P = n + 1 and
A19: for x being Element of K holds eval (P,x) = Det ((Delete (A,1,1)) + (x * (1. (K,n)))) by A2, A4;
take PP = <%((A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1)))),(((1. (K,(n + 1))) * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1))))%> *' P; ::_thesis: ( len PP = (n + 1) + 1 & ( for x being Element of K holds eval (PP,x) = Sum ((LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) | (k + 1)) ) )
 P . n <> 0. K by A18, ALGSEQ_1:10;
then  (<%((A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1)))),(((1. (K,(n + 1))) * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1))))%> . ((len <%((A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1)))),(((1. (K,(n + 1))) * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1))))%>) -' 1)) * (P . ((len P) -' 1)) <> 0. K by A4, A18, A17, A16, VECTSP_1:12;
hence  len PP = ((n + 1) + 2) - 1 by A18, A17, POLYNOM4:10
.= (n + 1) + 1 ;
::_thesis: for x being Element of K holds eval (PP,x) = Sum ((LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) | (k + 1))
let x be Element of K; ::_thesis: eval (PP,x) = Sum ((LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) | (k + 1))
A20: (Delete (A,1,1)) + (x * (1. (K,n))) = (Delete (A,1,1)) + (x * (Delete ((1. (K,(n + 1))),1,1))) by A6, A4, Th6
.= (Delete (A,1,1)) + (Delete ((x * (1. (K,(n + 1)))),1,1)) by A12, A14, Th5
.= Delete ((A + (x * (1. (K,(n + 1))))),1,1) by A6, Th4 ;
A21: ((A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1)))) + ((((1. (K,(n + 1))) * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1)))) * x) = ((A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1)))) + ((((1. (K,(n + 1))) * (1,(k + 1))) * x) * ((power K) . ((- (1_ K)),((k + 1) + 1)))) by GROUP_1:def_3
.= ((A * (1,(k + 1))) + (((1. (K,(n + 1))) * (1,(k + 1))) * x)) * ((power K) . ((- (1_ K)),((k + 1) + 1))) by VECTSP_1:def_2
.= ((A * (1,(k + 1))) + ((x * (1. (K,(n + 1)))) * (1,(k + 1)))) * ((power K) . ((- (1_ K)),((k + 1) + 1))) by A3, A13, MATRIX_3:def_5
.= ((A + (x * (1. (K,(n + 1))))) * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1))) by A13, MATRIX_3:def_3 ;
set L = LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1);
A22: dom (LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) = Seg (len (LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1))) by FINSEQ_1:def_3;
A23: len (LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) = n + 1 by LAPLACE:def_7;
A24: eval ((<%((A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1)))),(((1. (K,(n + 1))) * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1))))%> *' P),x) = (eval (<%((A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1)))),(((1. (K,(n + 1))) * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1))))%>,x)) * (eval (P,x)) by POLYNOM4:24
.= (eval (<%((A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1)))),(((1. (K,(n + 1))) * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1))))%>,x)) * (Det ((Delete (A,1,1)) + (x * (1. (K,n))))) by A19
.= (Minor ((A + (x * (1. (K,(n + 1))))),1,1)) * (((A + (x * (1. (K,(n + 1))))) * (1,1)) * ((power K) . ((- (1_ K)),((k + 1) + 1)))) by A14, A21, A20, POLYNOM5:44
.= ((A + (x * (1. (K,(n + 1))))) * (1,1)) * (Cofactor ((A + (x * (1. (K,(n + 1))))),1,1)) by A14, GROUP_1:def_3
.= (LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) . 1 by A6, A22, A23, LAPLACE:def_7 ;
thus  Sum ((LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) | (k + 1)) = Sum <*((LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) /. 1)*> by A14, A23, CARD_1:27, FINSEQ_5:20
.= Sum <*(eval ((<%((A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1)))),(((1. (K,(n + 1))) * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1))))%> *' P),x))*> by A6, A22, A23, A24, PARTFUN1:def_6
.= eval (PP,x) by FINSOP_1:11 ; ::_thesis: verum
end;
supposeA25: k >= 1 ; ::_thesis: ex P being Polynomial of K st
( len P = (n + 1) + 1 & ( for x being Element of K holds eval (P,x) = Sum ((LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) | (k + 1)) ) )
consider P1 being Polynomial of K such that
A26: len P1 <= n + 1 and
A27: for x being Element of K holds eval (P1,x) = Det ((Delete (A,1,(k + 1))) + (x * (Delete ((1. (K,(n + 1))),1,(k + 1))))) by A4, Th7;
consider P being Polynomial of K such that
A28: len P = (n + 1) + 1 and
A29: for x being Element of K holds eval (P,x) = Sum ((LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) | k) by A9, A11, A25, NAT_1:13;
take PP = P + (((A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1)))) * P1); ::_thesis: ( len PP = (n + 1) + 1 & ( for x being Element of K holds eval (PP,x) = Sum ((LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) | (k + 1)) ) )
 ( (A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1))) = 0. K or (A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1))) <> 0. K ) ;
then  len (((A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1)))) * P1) <= n + 1 by A26, POLYNOM5:24, POLYNOM5:25;
then A30: len (((A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1)))) * P1) < len P by A28, NAT_1:13;
hence  len PP = max ((len (((A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1)))) * P1)),(len P)) by POLYNOM4:7
.= (n + 1) + 1 by A28, A30, XXREAL_0:def_10 ;
::_thesis: for x being Element of K holds eval (PP,x) = Sum ((LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) | (k + 1))
let x be Element of K; ::_thesis: eval (PP,x) = Sum ((LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) | (k + 1))
set L = LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1);
A31: ( dom (LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) = Seg (len (LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1))) & len (LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) = n + 1 ) by FINSEQ_1:def_3, LAPLACE:def_7;
then A32: (LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) | (k + 1) = ((LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) | k) ^ <*((LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) . (k + 1))*> by A12, FINSEQ_5:10;
A33: k + 1 <> 1 by A25, NAT_1:13;
A34: (A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1))) = ((A * (1,(k + 1))) + (0. K)) * ((power K) . ((- (1_ K)),((k + 1) + 1))) by RLVECT_1:def_4
.= ((A * (1,(k + 1))) + (x * (0. K))) * ((power K) . ((- (1_ K)),((k + 1) + 1))) by VECTSP_1:7
.= ((A * (1,(k + 1))) + (x * ((1. (K,(n + 1))) * (1,(k + 1))))) * ((power K) . ((- (1_ K)),((k + 1) + 1))) by A3, A13, A33, MATRIX_1:def_11
.= ((A * (1,(k + 1))) + ((x * (1. (K,(n + 1)))) * (1,(k + 1)))) * ((power K) . ((- (1_ K)),((k + 1) + 1))) by A3, A13, MATRIX_3:def_5
.= ((A + (x * (1. (K,(n + 1))))) * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1))) by A13, MATRIX_3:def_3 ;
A35: (Delete (A,1,(k + 1))) + (x * (Delete ((1. (K,(n + 1))),1,(k + 1)))) = (Delete (A,1,(k + 1))) + (Delete ((x * (1. (K,(n + 1)))),1,(k + 1))) by A6, A12, Th5
.= Delete ((A + (x * (1. (K,(n + 1))))),1,(k + 1)) by A6, A12, Th4 ;
eval ((((A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1)))) * P1),x) = ((A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1)))) * (eval (P1,x)) by POLYNOM5:30
.= (Minor ((A + (x * (1. (K,(n + 1))))),1,(k + 1))) * (((A + (x * (1. (K,(n + 1))))) * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1)))) by A27, A34, A35
.= ((A + (x * (1. (K,(n + 1))))) * (1,(k + 1))) * (Cofactor ((A + (x * (1. (K,(n + 1))))),1,(k + 1))) by GROUP_1:def_3
.= (LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) . (k + 1) by A12, A31, LAPLACE:def_7 ;
hence  Sum ((LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) | (k + 1)) = (Sum ((LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) | k)) + (eval ((((A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1)))) * P1),x)) by A32, FVSUM_1:71
.= (eval (P,x)) + (eval ((((A * (1,(k + 1))) * ((power K) . ((- (1_ K)),((k + 1) + 1)))) * P1),x)) by A29
.= eval (PP,x) by POLYNOM4:19 ;
::_thesis: verum
end;
end;
end;
A36: S2[ 0 ] ;
 for k being Nat holds S2[k] from NAT_1:sch_2(A36, A8);
then consider P being Polynomial of K such that
A37: len P = (n + 1) + 1 and
A38: for x being Element of K holds eval (P,x) = Sum ((LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) | (n + 1)) by A5;
take  P ; ::_thesis: ( len P = (n + 1) + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * (1. (K,(n + 1))))) ) )
thus  len P = (n + 1) + 1 by A37; ::_thesis: for x being Element of K holds eval (P,x) = Det (A + (x * (1. (K,(n + 1)))))
let x be Element of K; ::_thesis: eval (P,x) = Det (A + (x * (1. (K,(n + 1)))))
set L = LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1);
 len (LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) = n + 1 by LAPLACE:def_7;
hence  eval (P,x) = Sum ((LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) | (len (LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)))) by A38
.= Sum (LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) by FINSEQ_1:58
.= Det (A + (x * (1. (K,(n + 1))))) by A6, LAPLACE:25 ;
::_thesis: verum
end;
A39: S1[ 0 ]
proof
let A be Matrix of 0 ,K; ::_thesis: ex P being Polynomial of K st
( len P = 0 + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * (1. (K,0)))) ) )
take P = 1_. K; ::_thesis: ( len P = 0 + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * (1. (K,0)))) ) )
thus  len P = 0 + 1 by POLYNOM4:4; ::_thesis: for x being Element of K holds eval (P,x) = Det (A + (x * (1. (K,0))))
let x be Element of K; ::_thesis: eval (P,x) = Det (A + (x * (1. (K,0))))
thus  Det (A + (x * (1. (K,0)))) = 1_ K by MATRIXR2:41
.= eval (P,x) by POLYNOM4:18 ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A39, A1);
hence  for A being Matrix of n,K ex P being Polynomial of K st
( len P = n + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * (1. (K,n)))) ) ) ; ::_thesis: verum
end;

Lm1:  for K being Field
for V1, V2 being VectSp of K
for f being linear-transformation of V1,V2
for W1 being Subspace of V1
for W2 being Subspace of V2
for F being Function of W1,W2 st F = f | W1 holds
F is linear-transformation of W1,W2
proof
let K be Field; ::_thesis: for V1, V2 being VectSp of K
for f being linear-transformation of V1,V2
for W1 being Subspace of V1
for W2 being Subspace of V2
for F being Function of W1,W2 st F = f | W1 holds
F is linear-transformation of W1,W2
let V1, V2 be VectSp of K; ::_thesis: for f being linear-transformation of V1,V2
for W1 being Subspace of V1
for W2 being Subspace of V2
for F being Function of W1,W2 st F = f | W1 holds
F is linear-transformation of W1,W2
let f be linear-transformation of V1,V2; ::_thesis: for W1 being Subspace of V1
for W2 being Subspace of V2
for F being Function of W1,W2 st F = f | W1 holds
F is linear-transformation of W1,W2
let W1 be Subspace of V1; ::_thesis: for W2 being Subspace of V2
for F being Function of W1,W2 st F = f | W1 holds
F is linear-transformation of W1,W2
let W2 be Subspace of V2; ::_thesis: for F being Function of W1,W2 st F = f | W1 holds
F is linear-transformation of W1,W2
let F be Function of W1,W2; ::_thesis: ( F = f | W1 implies F is linear-transformation of W1,W2 )
assume A1: F = f | W1 ; ::_thesis: F is linear-transformation of W1,W2
A2: now__::_thesis:_for_a_being_Scalar_of_K
for_w_being_Vector_of_W1_holds_F_._(a_*_w)_=_a_*_(F_._w)
let a be Scalar of K; ::_thesis: for w being Vector of W1 holds F . (a * w) = a * (F . w)
let w be Vector of W1; ::_thesis: F . (a * w) = a * (F . w)
thus F . (a * w) = a * ((f | W1) . w) by A1, MOD_2:def_2
.= a * (F . w) by A1, VECTSP_4:14 ; ::_thesis: verum
end;
now__::_thesis:_for_w1,_w2_being_Vector_of_W1_holds_F_._(w1_+_w2)_=_(F_._w1)_+_(F_._w2)
let w1, w2 be Vector of W1; ::_thesis: F . (w1 + w2) = (F . w1) + (F . w2)
thus F . (w1 + w2) = ((f | W1) . w1) + ((f | W1) . w2) by A1, VECTSP_1:def_20
.= (F . w1) + (F . w2) by A1, VECTSP_4:13 ; ::_thesis: verum
end;
then  ( F is additive & F is homogeneous ) by A2, VECTSP_1:def_20, MOD_2:def_2;
hence  F is linear-transformation of W1,W2 ; ::_thesis: verum
end;

registration
let K be Field;
cluster non empty non trivial right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed finite-dimensional for VectSpStr over K;
existence
 ex b1 being VectSp of K st
( not b1 is trivial & b1 is finite-dimensional )
proof
take V = 1 -VectSp_over K; ::_thesis: ( not V is trivial & V is finite-dimensional )
 dim V = 1 by MATRIX13:112;
then  ex v being Vector of V st
( v <> 0. V & (Omega). V = Lin {v} ) by VECTSP_9:30;
hence  ( not V is trivial & V is finite-dimensional ) by STRUCT_0:def_18; ::_thesis: verum
end;
end;

begin

definition
let R be non empty doubleLoopStr ;
let V be non empty VectSpStr over R;
let IT be Function of V,V;
attrIT is with_eigenvalues  means :Def1: :: VECTSP11:def 1
 ex v being Vector of V ex a being Scalar of R st
( v <> 0. V & IT . v = a * v );
end;

:: deftheorem Def1 defines with_eigenvalues VECTSP11:def_1_:_
 for R being non empty doubleLoopStr
for V being non empty VectSpStr over R
for IT being Function of V,V holds
( IT is with_eigenvalues iff ex v being Vector of V ex a being Scalar of R st
( v <> 0. V & IT . v = a * v ) );

        Lm2:  for K being Field
for V being non trivial VectSp of K holds
( id V is with_eigenvalues & ex v being Vector of V st
( v <> 0. V & (id V) . v = (1_ K) * v ) )
proof
let K be Field; ::_thesis: for V being non trivial VectSp of K holds
( id V is with_eigenvalues & ex v being Vector of V st
( v <> 0. V & (id V) . v = (1_ K) * v ) )
let V be non trivial VectSp of K; ::_thesis: ( id V is with_eigenvalues & ex v being Vector of V st
( v <> 0. V & (id V) . v = (1_ K) * v ) )
consider v being Vector of V such that
A1: v <> 0. V by STRUCT_0:def_18;
(id V) . v = v by FUNCT_1:17
.= (1_ K) * v by VECTSP_1:def_17 ;
hence  ( id V is with_eigenvalues & ex v being Vector of V st
( v <> 0. V & (id V) . v = (1_ K) * v ) ) by A1, Def1; ::_thesis: verum
end;

registration
let K be Field;
let V be non trivial VectSp of K;
cluster Relation-like the carrier of V -defined the carrier of V -valued Function-like non empty total quasi_total additive homogeneous with_eigenvalues for Element of bool [: the carrier of V, the carrier of V:];
existence
 ex b1 being linear-transformation of V,V st b1 is with_eigenvalues
proof
take  id V ; ::_thesis: id V is with_eigenvalues
thus  id V is with_eigenvalues by Lm2; ::_thesis: verum
end;
end;

definition
let R be non empty doubleLoopStr ;
let V be non empty VectSpStr over R;
let f be Function of V,V;
assume A1: f is with_eigenvalues ;
mode eigenvalue of f ->  Element of R means :Def2: :: VECTSP11:def 2
 ex v being Vector of V st
( v <> 0. V & f . v = it * v );
existence
 ex b1 being Element of R ex v being Vector of V st
( v <> 0. V & f . v = b1 * v )
proof
 ex v being Vector of V ex a being Scalar of R st
( v <> 0. V & f . v = a * v ) by A1, Def1;
hence  ex b1 being Element of R ex v being Vector of V st
( v <> 0. V & f . v = b1 * v ) ; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines eigenvalue VECTSP11:def_2_:_
 for R being non empty doubleLoopStr
for V being non empty VectSpStr over R
for f being Function of V,V st f is with_eigenvalues holds
for b4 being Element of R holds
( b4 is eigenvalue of f iff ex v being Vector of V st
( v <> 0. V & f . v = b4 * v ) );

definition
let R be non empty doubleLoopStr ;
let V be non empty VectSpStr over R;
let f be Function of V,V;
let L be Scalar of R;
assume A1: ( f is with_eigenvalues & L is eigenvalue of f ) ;
mode eigenvector of f,L ->  Vector of V means :Def3: :: VECTSP11:def 3
f . it = L * it;
existence
 ex b1 being Vector of V st f . b1 = L * b1
proof
 ex v being Vector of V st
( v <> 0. V & f . v = L * v ) by A1, Def2;
hence  ex b1 being Vector of V st f . b1 = L * b1 ; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines eigenvector VECTSP11:def_3_:_
 for R being non empty doubleLoopStr
for V being non empty VectSpStr over R
for f being Function of V,V
for L being Scalar of R st f is with_eigenvalues & L is eigenvalue of f holds
for b5 being Vector of V holds
( b5 is eigenvector of f,L iff f . b5 = L * b5 );

theorem :: VECTSP11:9
for K being Field
for V being non trivial VectSp of K
for w being Vector of V
for a being Element of K st a <> 0. K holds
for f being with_eigenvalues Function of V,V
for L being eigenvalue of f holds
( a * f is with_eigenvalues & a * L is eigenvalue of a * f & ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) & ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) )
proof
let K be Field; ::_thesis: for V being non trivial VectSp of K
for w being Vector of V
for a being Element of K st a <> 0. K holds
for f being with_eigenvalues Function of V,V
for L being eigenvalue of f holds
( a * f is with_eigenvalues & a * L is eigenvalue of a * f & ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) & ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) )
let V be non trivial VectSp of K; ::_thesis: for w being Vector of V
for a being Element of K st a <> 0. K holds
for f being with_eigenvalues Function of V,V
for L being eigenvalue of f holds
( a * f is with_eigenvalues & a * L is eigenvalue of a * f & ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) & ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) )
let w be Vector of V; ::_thesis: for a being Element of K st a <> 0. K holds
for f being with_eigenvalues Function of V,V
for L being eigenvalue of f holds
( a * f is with_eigenvalues & a * L is eigenvalue of a * f & ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) & ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) )
let a be Element of K; ::_thesis: ( a <> 0. K implies for f being with_eigenvalues Function of V,V
for L being eigenvalue of f holds
( a * f is with_eigenvalues & a * L is eigenvalue of a * f & ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) & ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) ) )
assume A1: a <> 0. K ; ::_thesis: for f being with_eigenvalues Function of V,V
for L being eigenvalue of f holds
( a * f is with_eigenvalues & a * L is eigenvalue of a * f & ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) & ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) )
let f be with_eigenvalues Function of V,V; ::_thesis: for L being eigenvalue of f holds
( a * f is with_eigenvalues & a * L is eigenvalue of a * f & ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) & ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) )
let L be eigenvalue of f; ::_thesis: ( a * f is with_eigenvalues & a * L is eigenvalue of a * f & ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) & ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) )
consider v being Vector of V such that
A2: v <> 0. V and
A3: f . v = L * v by Def2;
A4: (a * f) . v = a * (L * v) by A3, MATRLIN:def_4
.= (a * L) * v by VECTSP_1:def_16 ;
hence A5: a * f is with_eigenvalues by A2, Def1; ::_thesis: ( a * L is eigenvalue of a * f & ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) & ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) )
hence A6: a * L is eigenvalue of a * f by A2, A4, Def2; ::_thesis: ( ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) & ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) )
hereby  ::_thesis: ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L )
assume A7: w is eigenvector of f,L ; ::_thesis: w is eigenvector of a * f,a * L
(a * f) . w = a * (f . w) by MATRLIN:def_4
.= a * (L * w) by A7, Def3
.= (a * L) * w by VECTSP_1:def_16 ;
hence  w is eigenvector of a * f,a * L by A5, A6, Def3; ::_thesis: verum
end;
assume A8: w is eigenvector of a * f,a * L ; ::_thesis: w is eigenvector of f,L
a * (f . w) = (a * f) . w by MATRLIN:def_4
.= (a * L) * w by A5, A6, A8, Def3
.= a * (L * w) by VECTSP_1:def_16 ;
then  0. V = (a * (f . w)) + (- (a * (L * w))) by VECTSP_1:16
.= (a * (f . w)) + (a * (- (L * w))) by VECTSP_1:22
.= a * ((f . w) - (L * w)) by VECTSP_1:def_14 ;
then  (f . w) - (L * w) = 0. V by A1, VECTSP_1:15;
then  - (f . w) = - (L * w) by VECTSP_1:16;
then  f . w = L * w by RLVECT_1:18;
hence  w is eigenvector of f,L by Def3; ::_thesis: verum
end;

theorem :: VECTSP11:10
for K being Field
for V being non trivial VectSp of K
for f1, f2 being with_eigenvalues Function of V,V
for L1, L2 being Scalar of K st L1 is eigenvalue of f1 & L2 is eigenvalue of f2 & ex v being Vector of V st
( v is eigenvector of f1,L1 & v is eigenvector of f2,L2 & v <> 0. V ) holds
( f1 + f2 is with_eigenvalues & L1 + L2 is eigenvalue of f1 + f2 & ( for w being Vector of V st w is eigenvector of f1,L1 & w is eigenvector of f2,L2 holds
w is eigenvector of f1 + f2,L1 + L2 ) )
proof
let K be Field; ::_thesis: for V being non trivial VectSp of K
for f1, f2 being with_eigenvalues Function of V,V
for L1, L2 being Scalar of K st L1 is eigenvalue of f1 & L2 is eigenvalue of f2 & ex v being Vector of V st
( v is eigenvector of f1,L1 & v is eigenvector of f2,L2 & v <> 0. V ) holds
( f1 + f2 is with_eigenvalues & L1 + L2 is eigenvalue of f1 + f2 & ( for w being Vector of V st w is eigenvector of f1,L1 & w is eigenvector of f2,L2 holds
w is eigenvector of f1 + f2,L1 + L2 ) )
let V be non trivial VectSp of K; ::_thesis: for f1, f2 being with_eigenvalues Function of V,V
for L1, L2 being Scalar of K st L1 is eigenvalue of f1 & L2 is eigenvalue of f2 & ex v being Vector of V st
( v is eigenvector of f1,L1 & v is eigenvector of f2,L2 & v <> 0. V ) holds
( f1 + f2 is with_eigenvalues & L1 + L2 is eigenvalue of f1 + f2 & ( for w being Vector of V st w is eigenvector of f1,L1 & w is eigenvector of f2,L2 holds
w is eigenvector of f1 + f2,L1 + L2 ) )
let f1, f2 be with_eigenvalues Function of V,V; ::_thesis: for L1, L2 being Scalar of K st L1 is eigenvalue of f1 & L2 is eigenvalue of f2 & ex v being Vector of V st
( v is eigenvector of f1,L1 & v is eigenvector of f2,L2 & v <> 0. V ) holds
( f1 + f2 is with_eigenvalues & L1 + L2 is eigenvalue of f1 + f2 & ( for w being Vector of V st w is eigenvector of f1,L1 & w is eigenvector of f2,L2 holds
w is eigenvector of f1 + f2,L1 + L2 ) )
let L1, L2 be Scalar of K; ::_thesis: ( L1 is eigenvalue of f1 & L2 is eigenvalue of f2 & ex v being Vector of V st
( v is eigenvector of f1,L1 & v is eigenvector of f2,L2 & v <> 0. V ) implies ( f1 + f2 is with_eigenvalues & L1 + L2 is eigenvalue of f1 + f2 & ( for w being Vector of V st w is eigenvector of f1,L1 & w is eigenvector of f2,L2 holds
w is eigenvector of f1 + f2,L1 + L2 ) ) )
set g = f1 + f2;
assume that
A1: L1 is eigenvalue of f1 and
A2: L2 is eigenvalue of f2 ; ::_thesis: ( for v being Vector of V holds
( not v is eigenvector of f1,L1 or not v is eigenvector of f2,L2 or not v <> 0. V ) or ( f1 + f2 is with_eigenvalues & L1 + L2 is eigenvalue of f1 + f2 & ( for w being Vector of V st w is eigenvector of f1,L1 & w is eigenvector of f2,L2 holds
w is eigenvector of f1 + f2,L1 + L2 ) ) )
given v being Vector of V such that A3: v is eigenvector of f1,L1 and
A4: v is eigenvector of f2,L2 and
A5: v <> 0. V ; ::_thesis: ( f1 + f2 is with_eigenvalues & L1 + L2 is eigenvalue of f1 + f2 & ( for w being Vector of V st w is eigenvector of f1,L1 & w is eigenvector of f2,L2 holds
w is eigenvector of f1 + f2,L1 + L2 ) )
A6: (f1 + f2) . v = (f1 . v) + (f2 . v) by MATRLIN:def_3
.= (L1 * v) + (f2 . v) by A1, A3, Def3
.= (L1 * v) + (L2 * v) by A2, A4, Def3
.= (L1 + L2) * v by VECTSP_1:def_15 ;
hence A7: f1 + f2 is with_eigenvalues by A5, Def1; ::_thesis: ( L1 + L2 is eigenvalue of f1 + f2 & ( for w being Vector of V st w is eigenvector of f1,L1 & w is eigenvector of f2,L2 holds
w is eigenvector of f1 + f2,L1 + L2 ) )
hence A8: L1 + L2 is eigenvalue of f1 + f2 by A5, A6, Def2; ::_thesis: for w being Vector of V st w is eigenvector of f1,L1 & w is eigenvector of f2,L2 holds
w is eigenvector of f1 + f2,L1 + L2
let w be Vector of V; ::_thesis: ( w is eigenvector of f1,L1 & w is eigenvector of f2,L2 implies w is eigenvector of f1 + f2,L1 + L2 )
assume that
A9: w is eigenvector of f1,L1 and
A10: w is eigenvector of f2,L2 ; ::_thesis: w is eigenvector of f1 + f2,L1 + L2
(f1 + f2) . w = (f1 . w) + (f2 . w) by MATRLIN:def_3
.= (L1 * w) + (f2 . w) by A1, A9, Def3
.= (L1 * w) + (L2 * w) by A2, A10, Def3
.= (L1 + L2) * w by VECTSP_1:def_15 ;
hence  w is eigenvector of f1 + f2,L1 + L2 by A7, A8, Def3; ::_thesis: verum
end;

theorem Th11: :: VECTSP11:11
for K being Field
for V being non trivial VectSp of K holds
( id V is with_eigenvalues & 1_ K is eigenvalue of id V & ( for v being Vector of V holds v is eigenvector of id V, 1_ K ) )
proof
let K be Field; ::_thesis: for V being non trivial VectSp of K holds
( id V is with_eigenvalues & 1_ K is eigenvalue of id V & ( for v being Vector of V holds v is eigenvector of id V, 1_ K ) )
let V be non trivial VectSp of K; ::_thesis: ( id V is with_eigenvalues & 1_ K is eigenvalue of id V & ( for v being Vector of V holds v is eigenvector of id V, 1_ K ) )
thus A1: id V is with_eigenvalues by Lm2; ::_thesis: ( 1_ K is eigenvalue of id V & ( for v being Vector of V holds v is eigenvector of id V, 1_ K ) )
 ex v being Vector of V st
( v <> 0. V & (id V) . v = (1_ K) * v ) by Lm2;
hence A2: 1_ K is eigenvalue of id V by A1, Def2; ::_thesis: for v being Vector of V holds v is eigenvector of id V, 1_ K
let w be Vector of V; ::_thesis: w is eigenvector of id V, 1_ K
(id V) . w = w by FUNCT_1:17
.= (1_ K) * w by VECTSP_1:def_17 ;
hence  w is eigenvector of id V, 1_ K by A1, A2, Def3; ::_thesis: verum
end;

theorem :: VECTSP11:12
for K being Field
for V being non trivial VectSp of K
for L being eigenvalue of id V holds L = 1_ K
proof
let K be Field; ::_thesis: for V being non trivial VectSp of K
for L being eigenvalue of id V holds L = 1_ K
let V be non trivial VectSp of K; ::_thesis: for L being eigenvalue of id V holds L = 1_ K
let L be eigenvalue of id V; ::_thesis: L = 1_ K
 id V is with_eigenvalues by Th11;
then consider v being Vector of V such that
A1: v <> 0. V and
A2: (id V) . v = L * v by Def2;
L * v = v by A2, FUNCT_1:17
.= (1_ K) * v by VECTSP_1:def_17 ;
hence  L = 1_ K by A1, VECTSP10:4; ::_thesis: verum
end;

theorem :: VECTSP11:13
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 st not ker f is trivial holds
( f is with_eigenvalues & 0. K is eigenvalue of f )
proof
let K be Field; ::_thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1 st not ker f is trivial holds
( f is with_eigenvalues & 0. K is eigenvalue of f )
let V1 be VectSp of K; ::_thesis: for f being linear-transformation of V1,V1 st not ker f is trivial holds
( f is with_eigenvalues & 0. K is eigenvalue of f )
let f be linear-transformation of V1,V1; ::_thesis: ( not ker f is trivial implies ( f is with_eigenvalues & 0. K is eigenvalue of f ) )
assume  not ker f is trivial ; ::_thesis: ( f is with_eigenvalues & 0. K is eigenvalue of f )
then consider v being Vector of (ker f) such that
A1: v <> 0. (ker f) by STRUCT_0:def_18;
reconsider v = v as Vector of V1 by VECTSP_4:10;
A2: f . v = 0. V1 by RANKNULL:14
.= (0. K) * v by VECTSP_1:14 ;
A3: v <> 0. V1 by A1, VECTSP_4:11;
then  f is with_eigenvalues by A2, Def1;
hence  ( f is with_eigenvalues & 0. K is eigenvalue of f ) by A3, A2, Def2; ::_thesis: verum
end;

theorem Th14: :: VECTSP11:14
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K holds
( ( f is with_eigenvalues & L is eigenvalue of f ) iff not ker (f + ((- L) * (id V1))) is trivial )
proof
let K be Field; ::_thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K holds
( ( f is with_eigenvalues & L is eigenvalue of f ) iff not ker (f + ((- L) * (id V1))) is trivial )
let V1 be VectSp of K; ::_thesis: for f being linear-transformation of V1,V1
for L being Scalar of K holds
( ( f is with_eigenvalues & L is eigenvalue of f ) iff not ker (f + ((- L) * (id V1))) is trivial )
let f be linear-transformation of V1,V1; ::_thesis: for L being Scalar of K holds
( ( f is with_eigenvalues & L is eigenvalue of f ) iff not ker (f + ((- L) * (id V1))) is trivial )
let L be Scalar of K; ::_thesis: ( ( f is with_eigenvalues & L is eigenvalue of f ) iff not ker (f + ((- L) * (id V1))) is trivial )
hereby  ::_thesis: ( not ker (f + ((- L) * (id V1))) is trivial implies ( f is with_eigenvalues & L is eigenvalue of f ) )
assume  ( f is with_eigenvalues & L is eigenvalue of f ) ; ::_thesis: not ker (f + ((- L) * (id V1))) is trivial
then consider v1 being Vector of V1 such that
A1: v1 <> 0. V1 and
A2: f . v1 = L * v1 by Def2;
(f + ((- L) * (id V1))) . v1 = (f . v1) + (((- L) * (id V1)) . v1) by MATRLIN:def_3
.= (f . v1) + ((- L) * ((id V1) . v1)) by MATRLIN:def_4
.= (f . v1) + ((- L) * v1) by FUNCT_1:17
.= (L + (- L)) * v1 by A2, VECTSP_1:def_15
.= (0. K) * v1 by VECTSP_1:19
.= 0. V1 by VECTSP_1:15 ;
then  v1 in ker (f + ((- L) * (id V1))) by RANKNULL:10;
then A3: v1 is Element of (ker (f + ((- L) * (id V1)))) by STRUCT_0:def_5;
 v1 <> 0. (ker (f + ((- L) * (id V1)))) by A1, VECTSP_4:11;
hence  not ker (f + ((- L) * (id V1))) is trivial by A3, STRUCT_0:def_18; ::_thesis: verum
end;
assume  not ker (f + ((- L) * (id V1))) is trivial ; ::_thesis: ( f is with_eigenvalues & L is eigenvalue of f )
then consider v being Vector of (ker (f + ((- L) * (id V1)))) such that
A4: v <> 0. (ker (f + ((- L) * (id V1)))) by STRUCT_0:def_18;
A5: v in ker (f + ((- L) * (id V1))) by STRUCT_0:def_5;
reconsider v = v as Vector of V1 by VECTSP_4:10;
0. V1 = (f + ((- L) * (id V1))) . v by A5, RANKNULL:10
.= (f . v) + (((- L) * (id V1)) . v) by MATRLIN:def_3
.= (f . v) + ((- L) * ((id V1) . v)) by MATRLIN:def_4
.= (f . v) + ((- L) * v) by FUNCT_1:17 ;
then A6: f . v = - ((- L) * v) by VECTSP_1:16
.= (- (- L)) * v by VECTSP_1:21
.= L * v by RLVECT_1:17 ;
A7: v <> 0. V1 by A4, VECTSP_4:11;
then  f is with_eigenvalues by A6, Def1;
hence  ( f is with_eigenvalues & L is eigenvalue of f ) by A6, A7, Def2; ::_thesis: verum
end;

theorem Th15: :: VECTSP11:15
for K being Field
for L being Scalar of K
for V1 being finite-dimensional VectSp of K
for b1, b19 being OrdBasis of V1
for f being linear-transformation of V1,V1 holds
( ( f is with_eigenvalues & L is eigenvalue of f ) iff Det (AutEqMt ((f + ((- L) * (id V1))),b1,b19)) = 0. K )
proof
let K be Field; ::_thesis: for L being Scalar of K
for V1 being finite-dimensional VectSp of K
for b1, b19 being OrdBasis of V1
for f being linear-transformation of V1,V1 holds
( ( f is with_eigenvalues & L is eigenvalue of f ) iff Det (AutEqMt ((f + ((- L) * (id V1))),b1,b19)) = 0. K )
let L be Scalar of K; ::_thesis: for V1 being finite-dimensional VectSp of K
for b1, b19 being OrdBasis of V1
for f being linear-transformation of V1,V1 holds
( ( f is with_eigenvalues & L is eigenvalue of f ) iff Det (AutEqMt ((f + ((- L) * (id V1))),b1,b19)) = 0. K )
let V1 be finite-dimensional VectSp of K; ::_thesis: for b1, b19 being OrdBasis of V1
for f being linear-transformation of V1,V1 holds
( ( f is with_eigenvalues & L is eigenvalue of f ) iff Det (AutEqMt ((f + ((- L) * (id V1))),b1,b19)) = 0. K )
let b1, b19 be OrdBasis of V1; ::_thesis: for f being linear-transformation of V1,V1 holds
( ( f is with_eigenvalues & L is eigenvalue of f ) iff Det (AutEqMt ((f + ((- L) * (id V1))),b1,b19)) = 0. K )
let f be linear-transformation of V1,V1; ::_thesis: ( ( f is with_eigenvalues & L is eigenvalue of f ) iff Det (AutEqMt ((f + ((- L) * (id V1))),b1,b19)) = 0. K )
A1: dim V1 = dim V1 ;
hereby  ::_thesis: ( Det (AutEqMt ((f + ((- L) * (id V1))),b1,b19)) = 0. K implies ( f is with_eigenvalues & L is eigenvalue of f ) )
assume  ( f is with_eigenvalues & L is eigenvalue of f ) ; ::_thesis: Det (AutEqMt ((f + ((- L) * (id V1))),b1,b19)) = 0. K
then  not ker (f + ((- L) * (id V1))) is trivial by Th14;
hence  Det (AutEqMt ((f + ((- L) * (id V1))),b1,b19)) = 0. K by A1, MATRLIN2:50; ::_thesis: verum
end;
assume  Det (AutEqMt ((f + ((- L) * (id V1))),b1,b19)) = 0. K ; ::_thesis: ( f is with_eigenvalues & L is eigenvalue of f )
then  not ker (f + ((- L) * (id V1))) is trivial by A1, MATRLIN2:50;
hence  ( f is with_eigenvalues & L is eigenvalue of f ) by Th14; ::_thesis: verum
end;

theorem :: VECTSP11:16
for K being algebraic-closed Field
for V1 being non trivial finite-dimensional VectSp of K
for f being linear-transformation of V1,V1 holds f is with_eigenvalues
proof
let K be algebraic-closed Field; ::_thesis: for V1 being non trivial finite-dimensional VectSp of K
for f being linear-transformation of V1,V1 holds f is with_eigenvalues
let V1 be non trivial finite-dimensional VectSp of K; ::_thesis: for f being linear-transformation of V1,V1 holds f is with_eigenvalues
let f be linear-transformation of V1,V1; ::_thesis: f is with_eigenvalues
set b1 = the OrdBasis of V1;
set AutA = AutMt (f, the OrdBasis of V1, the OrdBasis of V1);
consider P being Polynomial of K such that
A1: len P = (len the OrdBasis of V1) + 1 and
A2: for x being Element of K holds eval (P,x) = Det ((AutMt (f, the OrdBasis of V1, the OrdBasis of V1)) + (x * (1. (K,(len the OrdBasis of V1))))) by Th8;
 ( dim V1 <> 0 & dim V1 = len the OrdBasis of V1 ) by MATRLIN2:21, MATRLIN2:42;
then  len P > 1 + 0 by A1, XREAL_1:8;
then  P is with_roots by POLYNOM5:def_8;
then consider L being Element of K such that
A3: L is_a_root_of P by POLYNOM5:def_7;
A4: Mx2Tran ((L * (AutMt ((id V1), the OrdBasis of V1, the OrdBasis of V1))), the OrdBasis of V1, the OrdBasis of V1) = L * (Mx2Tran ((AutMt ((id V1), the OrdBasis of V1, the OrdBasis of V1)), the OrdBasis of V1, the OrdBasis of V1)) by MATRLIN2:38
.= L * (id V1) by MATRLIN2:34
.= Mx2Tran ((AutMt ((L * (id V1)), the OrdBasis of V1, the OrdBasis of V1)), the OrdBasis of V1, the OrdBasis of V1) by MATRLIN2:34 ;
0. K = eval (P,L) by A3, POLYNOM5:def_6
.= Det ((AutMt (f, the OrdBasis of V1, the OrdBasis of V1)) + (L * (1. (K,(len the OrdBasis of V1))))) by A2
.= Det ((AutMt (f, the OrdBasis of V1, the OrdBasis of V1)) + (L * (AutMt ((id V1), the OrdBasis of V1, the OrdBasis of V1)))) by MATRLIN2:28
.= Det ((AutMt (f, the OrdBasis of V1, the OrdBasis of V1)) + (AutMt ((L * (id V1)), the OrdBasis of V1, the OrdBasis of V1))) by A4, MATRLIN2:39
.= Det (AutMt ((f + (L * (id V1))), the OrdBasis of V1, the OrdBasis of V1)) by MATRLIN:42
.= Det (AutMt ((f + ((- (- L)) * (id V1))), the OrdBasis of V1, the OrdBasis of V1)) by RLVECT_1:17
.= Det (AutEqMt ((f + ((- (- L)) * (id V1))), the OrdBasis of V1, the OrdBasis of V1)) by MATRLIN2:def_2 ;
hence  f is with_eigenvalues by Th15; ::_thesis: verum
end;

theorem Th17: :: VECTSP11:17
for K being Field
for V1 being VectSp of K
for v1 being Vector of V1
for f being linear-transformation of V1,V1
for L being Scalar of K st f is with_eigenvalues & L is eigenvalue of f holds
( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) )
proof
let K be Field; ::_thesis: for V1 being VectSp of K
for v1 being Vector of V1
for f being linear-transformation of V1,V1
for L being Scalar of K st f is with_eigenvalues & L is eigenvalue of f holds
( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) )
let V1 be VectSp of K; ::_thesis: for v1 being Vector of V1
for f being linear-transformation of V1,V1
for L being Scalar of K st f is with_eigenvalues & L is eigenvalue of f holds
( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) )
let v1 be Vector of V1; ::_thesis: for f being linear-transformation of V1,V1
for L being Scalar of K st f is with_eigenvalues & L is eigenvalue of f holds
( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) )
let f be linear-transformation of V1,V1; ::_thesis: for L being Scalar of K st f is with_eigenvalues & L is eigenvalue of f holds
( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) )
let L be Scalar of K; ::_thesis: ( f is with_eigenvalues & L is eigenvalue of f implies ( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) ) )
assume A1: ( f is with_eigenvalues & L is eigenvalue of f ) ; ::_thesis: ( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) )
hereby  ::_thesis: ( v1 in ker (f + ((- L) * (id V1))) implies v1 is eigenvector of f,L )
assume  v1 is eigenvector of f,L ; ::_thesis: v1 in ker (f + ((- L) * (id V1)))
then A2: f . v1 = L * v1 by A1, Def3;
(f + ((- L) * (id V1))) . v1 = (f . v1) + (((- L) * (id V1)) . v1) by MATRLIN:def_3
.= (f . v1) + ((- L) * ((id V1) . v1)) by MATRLIN:def_4
.= (f . v1) + ((- L) * v1) by FUNCT_1:17
.= (L + (- L)) * v1 by A2, VECTSP_1:def_15
.= (0. K) * v1 by VECTSP_1:19
.= 0. V1 by VECTSP_1:15 ;
hence  v1 in ker (f + ((- L) * (id V1))) by RANKNULL:10; ::_thesis: verum
end;
assume  v1 in ker (f + ((- L) * (id V1))) ; ::_thesis: v1 is eigenvector of f,L
then  0. V1 = (f + ((- L) * (id V1))) . v1 by RANKNULL:10
.= (f . v1) + (((- L) * (id V1)) . v1) by MATRLIN:def_3
.= (f . v1) + ((- L) * ((id V1) . v1)) by MATRLIN:def_4
.= (f . v1) + ((- L) * v1) by FUNCT_1:17 ;
then f . v1 = - ((- L) * v1) by VECTSP_1:16
.= (- (- L)) * v1 by VECTSP_1:21
.= L * v1 by RLVECT_1:17 ;
hence  v1 is eigenvector of f,L by A1, Def3; ::_thesis: verum
end;

definition
let S be 1-sorted ;
let F be Function of S,S;
let n be Nat;
funcF |^ n ->  Function of S,S means :Def4: :: VECTSP11:def 4
 for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
it = Product (n |-> F9);
existence
 ex b1 being Function of S,S st
for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
b1 = Product (n |-> F9)
proof
reconsider F9 = F as Element of (GFuncs the carrier of S) by MONOID_0:73;
reconsider P = Product (n |-> F9) as Function of S,S by MONOID_0:73;
take  P ; ::_thesis: for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
P = Product (n |-> F9)
thus  for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
P = Product (n |-> F9) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of S,S st ( for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
b1 = Product (n |-> F9) ) & ( for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
b2 = Product (n |-> F9) ) holds
b1 = b2
proof
reconsider F9 = F as Element of (GFuncs the carrier of S) by MONOID_0:73;
let F1, F2 be Function of S,S; ::_thesis: ( ( for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
F1 = Product (n |-> F9) ) & ( for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
F2 = Product (n |-> F9) ) implies F1 = F2 )
assume that
A1: for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
F1 = Product (n |-> F9) and
A2: for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
F2 = Product (n |-> F9) ; ::_thesis: F1 = F2
thus F1 = Product (n |-> F9) by A1
.= F2 by A2 ; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines |^ VECTSP11:def_4_:_
 for S being 1-sorted
for F being Function of S,S
for n being Nat
for b4 being Function of S,S holds
( b4 = F |^ n iff for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
b4 = Product (n |-> F9) );


theorem Th18: :: VECTSP11:18
for S being 1-sorted
for F being Function of S,S holds F |^ 0 = id S
proof
let S be 1-sorted ; ::_thesis: for F being Function of S,S holds F |^ 0 = id S
let F be Function of S,S; ::_thesis: F |^ 0 = id S
set G = GFuncs the carrier of S;
reconsider F9 = F as Element of (GFuncs the carrier of S) by MONOID_0:73;
 0 |-> F9 = <*> the carrier of (GFuncs the carrier of S) ;
then  Product (0 |-> F9) = 1_ (GFuncs the carrier of S) by GROUP_4:8
.= the_unity_wrt the multF of (GFuncs the carrier of S) by GROUP_1:22
.= id S by MONOID_0:75 ;
hence  F |^ 0 = id S by Def4; ::_thesis: verum
end;

theorem Th19: :: VECTSP11:19
for S being 1-sorted
for F being Function of S,S holds F |^ 1 = F
proof
let S be 1-sorted ; ::_thesis: for F being Function of S,S holds F |^ 1 = F
let F be Function of S,S; ::_thesis: F |^ 1 = F
set G = GFuncs the carrier of S;
reconsider F9 = F as Element of (GFuncs the carrier of S) by MONOID_0:73;
Product (1 |-> F9) = Product <*F9*> by FINSEQ_2:59
.= F9 by GROUP_4:9 ;
hence  F |^ 1 = F by Def4; ::_thesis: verum
end;

theorem Th20: :: VECTSP11:20
for i, j being Nat
for S being 1-sorted
for F being Function of S,S holds F |^ (i + j) = (F |^ j) * (F |^ i)
proof
let i, j be Nat; ::_thesis: for S being 1-sorted
for F being Function of S,S holds F |^ (i + j) = (F |^ j) * (F |^ i)
let S be 1-sorted ; ::_thesis: for F being Function of S,S holds F |^ (i + j) = (F |^ j) * (F |^ i)
let F be Function of S,S; ::_thesis: F |^ (i + j) = (F |^ j) * (F |^ i)
set G = GFuncs the carrier of S;
reconsider Fg = F as Element of (GFuncs the carrier of S) by MONOID_0:73;
reconsider G = GFuncs the carrier of S as non empty unital associative multMagma ;
reconsider F9 = F as Element of G by MONOID_0:73;
Product ((i + j) |-> F9) = Product ((i |-> F9) ^ (j |-> F9)) by FINSEQ_2:123
.= (Product (i |-> F9)) * (Product (j |-> F9)) by GROUP_4:5
.= (Product (j |-> Fg)) (*) (Product (i |-> Fg)) by MONOID_0:70
.= (F |^ j) (*) (Product (i |-> Fg)) by Def4
.= (F |^ j) (*) (F |^ i) by Def4 ;
hence  F |^ (i + j) = (F |^ j) * (F |^ i) by Def4; ::_thesis: verum
end;

theorem :: VECTSP11:21
for i being Nat
for S being 1-sorted
for F being Function of S,S
for s1, s2 being Element of S
for n, m being Nat st (F |^ m) . s1 = s2 & (F |^ n) . s2 = s2 holds
(F |^ (m + (i * n))) . s1 = s2
proof
let i be Nat; ::_thesis: for S being 1-sorted
for F being Function of S,S
for s1, s2 being Element of S
for n, m being Nat st (F |^ m) . s1 = s2 & (F |^ n) . s2 = s2 holds
(F |^ (m + (i * n))) . s1 = s2
let S be 1-sorted ; ::_thesis: for F being Function of S,S
for s1, s2 being Element of S
for n, m being Nat st (F |^ m) . s1 = s2 & (F |^ n) . s2 = s2 holds
(F |^ (m + (i * n))) . s1 = s2
let F be Function of S,S; ::_thesis: for s1, s2 being Element of S
for n, m being Nat st (F |^ m) . s1 = s2 & (F |^ n) . s2 = s2 holds
(F |^ (m + (i * n))) . s1 = s2
let s1, s2 be Element of S; ::_thesis: for n, m being Nat st (F |^ m) . s1 = s2 & (F |^ n) . s2 = s2 holds
(F |^ (m + (i * n))) . s1 = s2
let n, m be Nat; ::_thesis: ( (F |^ m) . s1 = s2 & (F |^ n) . s2 = s2 implies (F |^ (m + (i * n))) . s1 = s2 )
assume that
A1: (F |^ m) . s1 = s2 and
A2: (F |^ n) . s2 = s2 ; ::_thesis: (F |^ (m + (i * n))) . s1 = s2
defpred S1[ Nat] means (F |^ (m + ($1 * n))) . s1 = s2;
A3: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A4: S1[i] ; ::_thesis: S1[i + 1]
A5: dom (F |^ (m + (i * n))) = the carrier of S by FUNCT_2:52;
percases ( the carrier of S <> {} or the carrier of S = {} ) ;
supposeA6: the carrier of S <> {} ; ::_thesis: S1[i + 1]
thus (F |^ (m + ((i + 1) * n))) . s1 = (F |^ (n + (m + (i * n)))) . s1
.= ((F |^ n) * (F |^ (m + (i * n)))) . s1 by Th20
.= s2 by A2, A4, A5, A6, FUNCT_1:13 ; ::_thesis: verum
end;
suppose the carrier of S = {} ; ::_thesis: S1[i + 1]
then  ( not s1 in dom (F |^ (m + ((i + 1) * n))) & s2 = {} ) by SUBSET_1:def_1;
hence  (F |^ (m + ((i + 1) * n))) . s1 = s2 by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
A7: S1[ 0 ] by A1;
 for i being Nat holds S1[i] from NAT_1:sch_2(A7, A3);
hence  (F |^ (m + (i * n))) . s1 = s2 ; ::_thesis: verum
end;

theorem :: VECTSP11:22
for n being Nat
for K being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V1 being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K
for W being Subspace of V1
for f being Function of V1,V1
for fW being Function of W,W st fW = f | W holds
(f |^ n) | W = fW |^ n
proof
let n be Nat; ::_thesis: for K being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V1 being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K
for W being Subspace of V1
for f being Function of V1,V1
for fW being Function of W,W st fW = f | W holds
(f |^ n) | W = fW |^ n
let K be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V1 being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K
for W being Subspace of V1
for f being Function of V1,V1
for fW being Function of W,W st fW = f | W holds
(f |^ n) | W = fW |^ n
let V1 be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K; ::_thesis: for W being Subspace of V1
for f being Function of V1,V1
for fW being Function of W,W st fW = f | W holds
(f |^ n) | W = fW |^ n
let W be Subspace of V1; ::_thesis: for f being Function of V1,V1
for fW being Function of W,W st fW = f | W holds
(f |^ n) | W = fW |^ n
let f be Function of V1,V1; ::_thesis: for fW being Function of W,W st fW = f | W holds
(f |^ n) | W = fW |^ n
let fW be Function of W,W; ::_thesis: ( fW = f | W implies (f |^ n) | W = fW |^ n )
assume A1: fW = f | W ; ::_thesis: (f |^ n) | W = fW |^ n
defpred S1[ Nat] means (f |^ $1) | W = fW |^ $1;
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; ::_thesis: S1[n + 1]
A4: rng (fW |^ n) c= [#] W by RELAT_1:def_19;
thus (f |^ (n + 1)) | W = ((f |^ 1) * (f |^ n)) | W by Th20
.= (f |^ 1) * ((f |^ n) | W) by RELAT_1:83
.= (f |^ 1) * ((id W) * (fW |^ n)) by A3, A4, RELAT_1:53
.= ((f |^ 1) * (id W)) * (fW |^ n) by RELAT_1:36
.= (f * (id W)) * (fW |^ n) by Th19
.= fW * (fW |^ n) by A1, RELAT_1:65
.= (fW |^ 1) * (fW |^ n) by Th19
.= fW |^ (n + 1) by Th20 ; ::_thesis: verum
end;
 [#] W c= [#] V1 by VECTSP_4:def_2;
then A5: [#] W = ([#] V1) /\ ([#] W) by XBOOLE_1:28;
(f |^ 0) | W = (id V1) | W by Th18
.= (id V1) * (id W) by RELAT_1:65
.= id W by A5, FUNCT_1:22
.= fW |^ 0 by Th18 ;
then A6: S1[ 0 ] ;
 for n being Nat holds S1[n] from NAT_1:sch_2(A6, A2);
hence  (f |^ n) | W = fW |^ n ; ::_thesis: verum
end;

registration
let K be Field;
let V1 be VectSp of K;
let f be linear-transformation of V1,V1;
let n be Nat;
clusterf |^ n ->  additive homogeneous ;
coherence
 ( f |^ n is homogeneous & f |^ n is additive )
proof
defpred S1[ Nat] means f |^ K is linear-transformation of V1,V1;
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume  S1[k] ; ::_thesis: S1[k + 1]
then reconsider fk = f |^ k as linear-transformation of V1,V1 ;
f |^ (k + 1) = fk * (f |^ 1) by Th20
.= fk * f by Th19 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
 f |^ 0 = id V1 by Th18;
then A2: S1[ 0 ] ;
 for k being Nat holds S1[k] from NAT_1:sch_2(A2, A1);
hence  ( f |^ n is homogeneous & f |^ n is additive ) ; ::_thesis: verum
end;
end;

theorem Th23: :: VECTSP11:23
for i, j being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for v1 being Vector of V1 st (f |^ i) . v1 = 0. V1 holds
(f |^ (i + j)) . v1 = 0. V1
proof
let i, j be Nat; ::_thesis: for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for v1 being Vector of V1 st (f |^ i) . v1 = 0. V1 holds
(f |^ (i + j)) . v1 = 0. V1
let K be Field; ::_thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1
for v1 being Vector of V1 st (f |^ i) . v1 = 0. V1 holds
(f |^ (i + j)) . v1 = 0. V1
let V1 be VectSp of K; ::_thesis: for f being linear-transformation of V1,V1
for v1 being Vector of V1 st (f |^ i) . v1 = 0. V1 holds
(f |^ (i + j)) . v1 = 0. V1
let f be linear-transformation of V1,V1; ::_thesis: for v1 being Vector of V1 st (f |^ i) . v1 = 0. V1 holds
(f |^ (i + j)) . v1 = 0. V1
let v1 be Vector of V1; ::_thesis: ( (f |^ i) . v1 = 0. V1 implies (f |^ (i + j)) . v1 = 0. V1 )
assume A1: (f |^ i) . v1 = 0. V1 ; ::_thesis: (f |^ (i + j)) . v1 = 0. V1
A2: dom (f |^ i) = the carrier of V1 by FUNCT_2:def_1;
thus (f |^ (i + j)) . v1 = ((f |^ j) * (f |^ i)) . v1 by Th20
.= (f |^ j) . (0. V1) by A1, A2, FUNCT_1:13
.= 0. V1 by RANKNULL:9 ; ::_thesis: verum
end;

begin

definition
let K be Field;
let V1 be VectSp of K;
let f be linear-transformation of V1,V1;
func UnionKers f ->  strict Subspace of V1 means :Def5: :: VECTSP11:def 5
 the carrier of it =  {  v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1  }  ;
existence
 ex b1 being strict Subspace of V1 st the carrier of b1 =  {  v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1  }
proof
set S =  {  v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1  }  ;
  {  v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1  }  c= the carrier of V1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1  }  or x in the carrier of V1 )
assume  x in  {  v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1  }  ; ::_thesis: x in the carrier of V1
then  ex v being Vector of V1 st
( x = v & ex n being Nat st (f |^ n) . v = 0. V1 ) ;
hence  x in the carrier of V1 ; ::_thesis: verum
end;
then reconsider S =  {  v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1  }  as Subset of V1 ;
(f |^ 0) . (0. V1) = (id V1) . (0. V1) by Th18
.= 0. V1 by FUNCT_1:17 ;
then A1: 0. V1 in S ;
A2: now__::_thesis:_for_v,_u_being_Element_of_V1_st_v_in_S_&_u_in_S_holds_
v_+_u_in_S
let v, u be Element of V1; ::_thesis: ( v in S & u in S implies v + u in S )
assume that
A3: v in S and
A4: u in S ; ::_thesis: v + u in S
 ex v9 being Vector of V1 st
( v9 = v & ex n being Nat st (f |^ n) . v9 = 0. V1 ) by A3;
then consider n being Nat such that
A5: (f |^ n) . v = 0. V1 ;
 ex u9 being Vector of V1 st
( u9 = u & ex m being Nat st (f |^ m) . u9 = 0. V1 ) by A4;
then consider m being Nat such that
A6: (f |^ m) . u = 0. V1 ;
now__::_thesis:_v_+_u_in_S
percases ( m <= n or m > n ) ;
suppose m <= n ; ::_thesis: v + u in S
then reconsider i = n - m as Nat by NAT_1:21;
(f |^ n) . (v + u) = ((f |^ n) . v) + ((f |^ (m + i)) . u) by VECTSP_1:def_20
.= (0. V1) + (0. V1) by A5, A6, Th23
.= 0. V1 by RLVECT_1:def_4 ;
hence  v + u in S ; ::_thesis: verum
end;
suppose m > n ; ::_thesis: v + u in S
then reconsider i = m - n as Nat by NAT_1:21;
(f |^ m) . (v + u) = ((f |^ m) . v) + ((f |^ (n + i)) . u) by VECTSP_1:def_20
.= (0. V1) + (0. V1) by A5, A6, Th23
.= 0. V1 by RLVECT_1:def_4 ;
hence  v + u in S ; ::_thesis: verum
end;
end;
end;
hence  v + u in S ; ::_thesis: verum
end;
now__::_thesis:_for_a_being_Element_of_K
for_v_being_Element_of_V1_st_v_in_S_holds_
a_*_v_in_S
let a be Element of K; ::_thesis: for v being Element of V1 st v in S holds
a * v in S
let v be Element of V1; ::_thesis: ( v in S implies a * v in S )
assume  v in S ; ::_thesis: a * v in S
then  ex v9 being Vector of V1 st
( v9 = v & ex n being Nat st (f |^ n) . v9 = 0. V1 ) ;
then consider n being Nat such that
A7: (f |^ n) . v = 0. V1 ;
(f |^ n) . (a * v) = a * (0. V1) by A7, MOD_2:def_2
.= 0. V1 by VECTSP_1:14 ;
hence  a * v in S ; ::_thesis: verum
end;
then  S is linearly-closed by A2, VECTSP_4:def_1;
hence  ex b1 being strict Subspace of V1 st the carrier of b1 =  {  v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1  }  by A1, VECTSP_4:34; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict Subspace of V1 st the carrier of b1 =  {  v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1  }  & the carrier of b2 =  {  v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1  }  holds
b1 = b2 by VECTSP_4:29;
end;

:: deftheorem Def5 defines UnionKers VECTSP11:def_5_:_
 for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for b4 being strict Subspace of V1 holds
( b4 = UnionKers f iff the carrier of b4 =  {  v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1  }  );

theorem Th24: :: VECTSP11:24
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for v1 being Vector of V1 holds
( v1 in UnionKers f iff ex n being Nat st (f |^ n) . v1 = 0. V1 )
proof
let K be Field; ::_thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1
for v1 being Vector of V1 holds
( v1 in UnionKers f iff ex n being Nat st (f |^ n) . v1 = 0. V1 )
let V1 be VectSp of K; ::_thesis: for f being linear-transformation of V1,V1
for v1 being Vector of V1 holds
( v1 in UnionKers f iff ex n being Nat st (f |^ n) . v1 = 0. V1 )
let f be linear-transformation of V1,V1; ::_thesis: for v1 being Vector of V1 holds
( v1 in UnionKers f iff ex n being Nat st (f |^ n) . v1 = 0. V1 )
let v1 be Vector of V1; ::_thesis: ( v1 in UnionKers f iff ex n being Nat st (f |^ n) . v1 = 0. V1 )
hereby  ::_thesis: ( ex n being Nat st (f |^ n) . v1 = 0. V1 implies v1 in UnionKers f )
assume  v1 in UnionKers f ; ::_thesis: ex n being Nat st (f |^ n) . v1 = 0. V1
then  v1 in the carrier of (UnionKers f) by STRUCT_0:def_5;
then  v1 in  {  w where w is Vector of V1 : ex n being Nat st (f |^ n) . w = 0. V1  }  by Def5;
then  ex w being Vector of V1 st
( v1 = w & ex m being Nat st (f |^ m) . w = 0. V1 ) ;
hence  ex n being Nat st (f |^ n) . v1 = 0. V1 ; ::_thesis: verum
end;
assume  ex n being Nat st (f |^ n) . v1 = 0. V1 ; ::_thesis: v1 in UnionKers f
then  v1 in  {  w where w is Vector of V1 : ex n being Nat st (f |^ n) . w = 0. V1  }  ;
then  v1 in the carrier of (UnionKers f) by Def5;
hence  v1 in UnionKers f by STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th25: :: VECTSP11:25
for i being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds ker (f |^ i) is Subspace of UnionKers f
proof
let i be Nat; ::_thesis: for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds ker (f |^ i) is Subspace of UnionKers f
let K be Field; ::_thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds ker (f |^ i) is Subspace of UnionKers f
let V1 be VectSp of K; ::_thesis: for f being linear-transformation of V1,V1 holds ker (f |^ i) is Subspace of UnionKers f
let f be linear-transformation of V1,V1; ::_thesis: ker (f |^ i) is Subspace of UnionKers f
 the carrier of (ker (f |^ i)) c= the carrier of (UnionKers f)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (ker (f |^ i)) or x in the carrier of (UnionKers f) )
assume  x in the carrier of (ker (f |^ i)) ; ::_thesis: x in the carrier of (UnionKers f)
then reconsider v = x as Element of (ker (f |^ i)) ;
 ( (f |^ i) . v = 0. V1 & v is Vector of V1 ) by RANKNULL:14, VECTSP_4:10;
then  x in UnionKers f by Th24;
hence  x in the carrier of (UnionKers f) by STRUCT_0:def_5; ::_thesis: verum
end;
hence  ker (f |^ i) is Subspace of UnionKers f by VECTSP_4:27; ::_thesis: verum
end;

theorem Th26: :: VECTSP11:26
for i, j being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds ker (f |^ i) is Subspace of ker (f |^ (i + j))
proof
let i, j be Nat; ::_thesis: for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds ker (f |^ i) is Subspace of ker (f |^ (i + j))
let K be Field; ::_thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds ker (f |^ i) is Subspace of ker (f |^ (i + j))
let V1 be VectSp of K; ::_thesis: for f being linear-transformation of V1,V1 holds ker (f |^ i) is Subspace of ker (f |^ (i + j))
let f be linear-transformation of V1,V1; ::_thesis: ker (f |^ i) is Subspace of ker (f |^ (i + j))
 the carrier of (ker (f |^ i)) c= the carrier of (ker (f |^ (i + j)))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (ker (f |^ i)) or x in the carrier of (ker (f |^ (i + j))) )
assume A1: x in the carrier of (ker (f |^ i)) ; ::_thesis: x in the carrier of (ker (f |^ (i + j)))
reconsider v = x as Vector of V1 by A1, VECTSP_4:10;
 (f |^ i) . v = 0. V1 by A1, RANKNULL:14;
then  (f |^ (i + j)) . v = 0. V1 by Th23;
then  v in ker (f |^ (i + j)) by RANKNULL:10;
hence  x in the carrier of (ker (f |^ (i + j))) by STRUCT_0:def_5; ::_thesis: verum
end;
hence  ker (f |^ i) is Subspace of ker (f |^ (i + j)) by VECTSP_4:27; ::_thesis: verum
end;

theorem :: VECTSP11:27
for K being Field
for V being finite-dimensional VectSp of K
for f being linear-transformation of V,V ex n being Nat st UnionKers f = ker (f |^ n)
proof
let K be Field; ::_thesis: for V being finite-dimensional VectSp of K
for f being linear-transformation of V,V ex n being Nat st UnionKers f = ker (f |^ n)
let V be finite-dimensional VectSp of K; ::_thesis: for f being linear-transformation of V,V ex n being Nat st UnionKers f = ker (f |^ n)
let f be linear-transformation of V,V; ::_thesis: ex n being Nat st UnionKers f = ker (f |^ n)
defpred S1[ Nat] means  for n being Nat holds dim (ker (f |^ n)) <= $1;
 S1[ dim (UnionKers f)]
proof
let n be Nat; ::_thesis: dim (ker (f |^ n)) <= dim (UnionKers f)
 ker (f |^ n) is Subspace of UnionKers f by Th25;
hence  dim (ker (f |^ n)) <= dim (UnionKers f) by VECTSP_9:25; ::_thesis: verum
end;
then A1: ex k being Nat st S1[k] ;
 ex k being Nat st
( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) ) from NAT_1:sch_5(A1);
then consider k being Nat such that
A2: S1[k] and
A3: for n being Nat st S1[n] holds
k <= n ;
 ex m being Nat st dim (ker (f |^ m)) = k
proof
assume A4: for m being Nat holds dim (ker (f |^ m)) <> k ; ::_thesis: contradiction
 dim (ker (f |^ 0)) <= k by A2;
then  dim (ker (f |^ 0)) < k by A4, XXREAL_0:1;
then reconsider k1 = k - 1 as Element of NAT by NAT_1:20;
now__::_thesis:_for_n_being_Nat_holds_dim_(ker_(f_|^_n))_<=_k1
let n be Nat; ::_thesis: dim (ker (f |^ n)) <= k1
 dim (ker (f |^ n)) <= k by A2;
then  dim (ker (f |^ n)) < k1 + 1 by A4, XXREAL_0:1;
hence  dim (ker (f |^ n)) <= k1 by NAT_1:13; ::_thesis: verum
end;
then  k1 + 1 <= k1 by A3;
hence  contradiction by NAT_1:16; ::_thesis: verum
end;
then consider m being Nat such that
A5: dim (ker (f |^ m)) = k ;
take  m ; ::_thesis: UnionKers f = ker (f |^ m)
assume A6: UnionKers f <> ker (f |^ m) ; ::_thesis: contradiction
 ker (f |^ m) is Subspace of UnionKers f by Th25;
then consider v being Element of (UnionKers f) such that
A7: not v in ker (f |^ m) by A6, VECTSP_4:32;
A8: v in UnionKers f by STRUCT_0:def_5;
reconsider v = v as Vector of V by VECTSP_4:10;
consider i being Nat such that
A9: (f |^ i) . v = 0. V by A8, Th24;
 i > m
proof
assume  i <= m ; ::_thesis: contradiction
then reconsider j = m - i as Element of NAT by NAT_1:21;
 (f |^ (j + i)) . v = 0. V by A9, Th23;
hence  contradiction by A7, RANKNULL:10; ::_thesis: verum
end;
then reconsider j = i - m as Element of NAT by NAT_1:21;
A10: ker (f |^ m) is Subspace of ker (f |^ (m + j)) by Th26;
then A11: k <= dim (ker (f |^ i)) by A5, VECTSP_9:25;
 (Omega). (ker (f |^ m)) <> (Omega). (ker (f |^ i)) by A7, A9, RANKNULL:10;
then  k <> dim (ker (f |^ i)) by A5, A10, VECTSP_9:28;
then  k < dim (ker (f |^ i)) by A11, XXREAL_0:1;
hence  contradiction by A2; ::_thesis: verum
end;

theorem Th28: :: VECTSP11:28
for n being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds f | (ker (f |^ n)) is linear-transformation of (ker (f |^ n)),(ker (f |^ n))
proof
let n be Nat; ::_thesis: for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds f | (ker (f |^ n)) is linear-transformation of (ker (f |^ n)),(ker (f |^ n))
let K be Field; ::_thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds f | (ker (f |^ n)) is linear-transformation of (ker (f |^ n)),(ker (f |^ n))
let V1 be VectSp of K; ::_thesis: for f being linear-transformation of V1,V1 holds f | (ker (f |^ n)) is linear-transformation of (ker (f |^ n)),(ker (f |^ n))
let f be linear-transformation of V1,V1; ::_thesis: f | (ker (f |^ n)) is linear-transformation of (ker (f |^ n)),(ker (f |^ n))
set KER = ker (f |^ n);
 rng (f | (ker (f |^ n))) c= the carrier of (ker (f |^ n))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (f | (ker (f |^ n))) or y in the carrier of (ker (f |^ n)) )
assume  y in rng (f | (ker (f |^ n))) ; ::_thesis: y in the carrier of (ker (f |^ n))
then consider x being set  such that
A1: x in dom (f | (ker (f |^ n))) and
A2: (f | (ker (f |^ n))) . x = y by FUNCT_1:def_3;
 x in the carrier of (ker (f |^ n)) by A1, FUNCT_2:def_1;
then A3: x in ker (f |^ n) by STRUCT_0:def_5;
then  x in V1 by VECTSP_4:9;
then reconsider v = x as Vector of V1 by STRUCT_0:def_5;
A4: dom f = the carrier of V1 by FUNCT_2:def_1;
 (f |^ n) . v = 0. V1 by A3, RANKNULL:10;
then  0. V1 = (f |^ (n + 1)) . v by Th23
.= ((f |^ n) * (f |^ 1)) . v by Th20
.= ((f |^ n) * f) . v by Th19
.= (f |^ n) . (f . v) by A4, FUNCT_1:13 ;
then A5: f . v in ker (f |^ n) by RANKNULL:10;
 y = f . v by A1, A2, FUNCT_1:47;
hence  y in the carrier of (ker (f |^ n)) by A5, STRUCT_0:def_5; ::_thesis: verum
end;
hence  f | (ker (f |^ n)) is linear-transformation of (ker (f |^ n)),(ker (f |^ n)) by Lm1, FUNCT_2:6; ::_thesis: verum
end;

theorem :: VECTSP11:29
for n being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K holds f | (ker ((f + (L * (id V1))) |^ n)) is linear-transformation of (ker ((f + (L * (id V1))) |^ n)),(ker ((f + (L * (id V1))) |^ n))
proof
let n be Nat; ::_thesis: for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K holds f | (ker ((f + (L * (id V1))) |^ n)) is linear-transformation of (ker ((f + (L * (id V1))) |^ n)),(ker ((f + (L * (id V1))) |^ n))
let K be Field; ::_thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K holds f | (ker ((f + (L * (id V1))) |^ n)) is linear-transformation of (ker ((f + (L * (id V1))) |^ n)),(ker ((f + (L * (id V1))) |^ n))
let V1 be VectSp of K; ::_thesis: for f being linear-transformation of V1,V1
for L being Scalar of K holds f | (ker ((f + (L * (id V1))) |^ n)) is linear-transformation of (ker ((f + (L * (id V1))) |^ n)),(ker ((f + (L * (id V1))) |^ n))
let f be linear-transformation of V1,V1; ::_thesis: for L being Scalar of K holds f | (ker ((f + (L * (id V1))) |^ n)) is linear-transformation of (ker ((f + (L * (id V1))) |^ n)),(ker ((f + (L * (id V1))) |^ n))
let L be Scalar of K; ::_thesis: f | (ker ((f + (L * (id V1))) |^ n)) is linear-transformation of (ker ((f + (L * (id V1))) |^ n)),(ker ((f + (L * (id V1))) |^ n))
set fid = f + (L * (id V1));
set KER = ker ((f + (L * (id V1))) |^ n);
reconsider fidK = (f + (L * (id V1))) | (ker ((f + (L * (id V1))) |^ n)) as linear-transformation of (ker ((f + (L * (id V1))) |^ n)),(ker ((f + (L * (id V1))) |^ n)) by Th28;
 rng (f | (ker ((f + (L * (id V1))) |^ n))) c= the carrier of (ker ((f + (L * (id V1))) |^ n))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (f | (ker ((f + (L * (id V1))) |^ n))) or y in the carrier of (ker ((f + (L * (id V1))) |^ n)) )
assume  y in rng (f | (ker ((f + (L * (id V1))) |^ n))) ; ::_thesis: y in the carrier of (ker ((f + (L * (id V1))) |^ n))
then consider x being set  such that
A1: x in dom (f | (ker ((f + (L * (id V1))) |^ n))) and
A2: (f | (ker ((f + (L * (id V1))) |^ n))) . x = y by FUNCT_1:def_3;
A3: x in the carrier of (ker ((f + (L * (id V1))) |^ n)) by A1, FUNCT_2:def_1;
then A4: x in ker ((f + (L * (id V1))) |^ n) by STRUCT_0:def_5;
then  x in V1 by VECTSP_4:9;
then reconsider v = x as Vector of V1 by STRUCT_0:def_5;
A5: (f | (ker ((f + (L * (id V1))) |^ n))) . v = f . v by A1, FUNCT_1:47;
 dom fidK = the carrier of (ker ((f + (L * (id V1))) |^ n)) by FUNCT_2:def_1;
then  ( fidK . v = (f + (L * (id V1))) . v & fidK /. v = fidK . v ) by A3, FUNCT_1:47, PARTFUN1:def_6;
then A6: (f + (L * (id V1))) . v in ker ((f + (L * (id V1))) |^ n) by STRUCT_0:def_5;
(f + (L * (id V1))) . v = (f . v) + ((L * (id V1)) . v) by MATRLIN:def_3
.= (f . v) + (L * ((id V1) . v)) by MATRLIN:def_4
.= (f . v) + (L * v) by FUNCT_1:18 ;
then A7: ((f + (L * (id V1))) . v) + ((- L) * v) = (f . v) + ((L * v) + ((- L) * v)) by RLVECT_1:def_3
.= (f . v) + ((L + (- L)) * v) by VECTSP_1:def_15
.= (f . v) + ((0. K) * v) by VECTSP_1:16
.= (f . v) + (0. V1) by VECTSP_1:14
.= f . v by RLVECT_1:def_4 ;
 (- L) * v in ker ((f + (L * (id V1))) |^ n) by A4, VECTSP_4:21;
then  f . v in ker ((f + (L * (id V1))) |^ n) by A7, A6, VECTSP_4:20;
hence  y in the carrier of (ker ((f + (L * (id V1))) |^ n)) by A2, A5, STRUCT_0:def_5; ::_thesis: verum
end;
hence  f | (ker ((f + (L * (id V1))) |^ n)) is linear-transformation of (ker ((f + (L * (id V1))) |^ n)),(ker ((f + (L * (id V1))) |^ n)) by Lm1, FUNCT_2:6; ::_thesis: verum
end;

theorem Th30: :: VECTSP11:30
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds f | (UnionKers f) is linear-transformation of (UnionKers f),(UnionKers f)
proof
let K be Field; ::_thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds f | (UnionKers f) is linear-transformation of (UnionKers f),(UnionKers f)
let V1 be VectSp of K; ::_thesis: for f being linear-transformation of V1,V1 holds f | (UnionKers f) is linear-transformation of (UnionKers f),(UnionKers f)
let f be linear-transformation of V1,V1; ::_thesis: f | (UnionKers f) is linear-transformation of (UnionKers f),(UnionKers f)
set U = UnionKers f;
 rng (f | (UnionKers f)) c= the carrier of (UnionKers f)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (f | (UnionKers f)) or y in the carrier of (UnionKers f) )
assume  y in rng (f | (UnionKers f)) ; ::_thesis: y in the carrier of (UnionKers f)
then consider x being set  such that
A1: x in dom (f | (UnionKers f)) and
A2: (f | (UnionKers f)) . x = y by FUNCT_1:def_3;
 x in the carrier of (UnionKers f) by A1, FUNCT_2:def_1;
then A3: x in UnionKers f by STRUCT_0:def_5;
then  x in V1 by VECTSP_4:9;
then reconsider v = x as Vector of V1 by STRUCT_0:def_5;
consider n being Nat such that
A4: (f |^ n) . v = 0. V1 by A3, Th24;
A5: dom f = [#] V1 by FUNCT_2:def_1;
0. V1 = (f |^ (n + 1)) . v by A4, Th23
.= ((f |^ n) * (f |^ 1)) . v by Th20
.= ((f |^ n) * f) . v by Th19
.= (f |^ n) . (f . v) by A5, FUNCT_1:13 ;
then A6: f . v in UnionKers f by Th24;
 y = f . v by A1, A2, FUNCT_1:47;
hence  y in the carrier of (UnionKers f) by A6, STRUCT_0:def_5; ::_thesis: verum
end;
hence  f | (UnionKers f) is linear-transformation of (UnionKers f),(UnionKers f) by Lm1, FUNCT_2:6; ::_thesis: verum
end;

theorem Th31: :: VECTSP11:31
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K holds f | (UnionKers (f + (L * (id V1)))) is linear-transformation of (UnionKers (f + (L * (id V1)))),(UnionKers (f + (L * (id V1))))
proof
let K be Field; ::_thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K holds f | (UnionKers (f + (L * (id V1)))) is linear-transformation of (UnionKers (f + (L * (id V1)))),(UnionKers (f + (L * (id V1))))
let V1 be VectSp of K; ::_thesis: for f being linear-transformation of V1,V1
for L being Scalar of K holds f | (UnionKers (f + (L * (id V1)))) is linear-transformation of (UnionKers (f + (L * (id V1)))),(UnionKers (f + (L * (id V1))))
let f be linear-transformation of V1,V1; ::_thesis: for L being Scalar of K holds f | (UnionKers (f + (L * (id V1)))) is linear-transformation of (UnionKers (f + (L * (id V1)))),(UnionKers (f + (L * (id V1))))
let L be Scalar of K; ::_thesis: f | (UnionKers (f + (L * (id V1)))) is linear-transformation of (UnionKers (f + (L * (id V1)))),(UnionKers (f + (L * (id V1))))
set fid = f + (L * (id V1));
set U = UnionKers (f + (L * (id V1)));
reconsider fidU = (f + (L * (id V1))) | (UnionKers (f + (L * (id V1)))) as linear-transformation of (UnionKers (f + (L * (id V1)))),(UnionKers (f + (L * (id V1)))) by Th30;
 rng (f | (UnionKers (f + (L * (id V1))))) c= the carrier of (UnionKers (f + (L * (id V1))))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (f | (UnionKers (f + (L * (id V1))))) or y in the carrier of (UnionKers (f + (L * (id V1)))) )
assume  y in rng (f | (UnionKers (f + (L * (id V1))))) ; ::_thesis: y in the carrier of (UnionKers (f + (L * (id V1))))
then consider x being set  such that
A1: x in dom (f | (UnionKers (f + (L * (id V1))))) and
A2: (f | (UnionKers (f + (L * (id V1))))) . x = y by FUNCT_1:def_3;
A3: x in the carrier of (UnionKers (f + (L * (id V1)))) by A1, FUNCT_2:def_1;
then A4: x in UnionKers (f + (L * (id V1))) by STRUCT_0:def_5;
then  x in V1 by VECTSP_4:9;
then reconsider v = x as Vector of V1 by STRUCT_0:def_5;
A5: (f | (UnionKers (f + (L * (id V1))))) . v = f . v by A1, FUNCT_1:47;
 dom fidU = the carrier of (UnionKers (f + (L * (id V1)))) by FUNCT_2:def_1;
then  ( fidU . v = (f + (L * (id V1))) . v & fidU /. v = fidU . v ) by A3, FUNCT_1:47, PARTFUN1:def_6;
then A6: (f + (L * (id V1))) . v in UnionKers (f + (L * (id V1))) by STRUCT_0:def_5;
(f + (L * (id V1))) . v = (f . v) + ((L * (id V1)) . v) by MATRLIN:def_3
.= (f . v) + (L * ((id V1) . v)) by MATRLIN:def_4
.= (f . v) + (L * v) by FUNCT_1:18 ;
then A7: ((f + (L * (id V1))) . v) + ((- L) * v) = (f . v) + ((L * v) + ((- L) * v)) by RLVECT_1:def_3
.= (f . v) + ((L + (- L)) * v) by VECTSP_1:def_15
.= (f . v) + ((0. K) * v) by VECTSP_1:16
.= (f . v) + (0. V1) by VECTSP_1:14
.= f . v by RLVECT_1:def_4 ;
 (- L) * v in UnionKers (f + (L * (id V1))) by A4, VECTSP_4:21;
then  f . v in UnionKers (f + (L * (id V1))) by A7, A6, VECTSP_4:20;
hence  y in the carrier of (UnionKers (f + (L * (id V1)))) by A2, A5, STRUCT_0:def_5; ::_thesis: verum
end;
hence  f | (UnionKers (f + (L * (id V1)))) is linear-transformation of (UnionKers (f + (L * (id V1)))),(UnionKers (f + (L * (id V1)))) by Lm1, FUNCT_2:6; ::_thesis: verum
end;

theorem Th32: :: VECTSP11:32
for n being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds f | (im (f |^ n)) is linear-transformation of (im (f |^ n)),(im (f |^ n))
proof
let n be Nat; ::_thesis: for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds f | (im (f |^ n)) is linear-transformation of (im (f |^ n)),(im (f |^ n))
let K be Field; ::_thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds f | (im (f |^ n)) is linear-transformation of (im (f |^ n)),(im (f |^ n))
let V1 be VectSp of K; ::_thesis: for f being linear-transformation of V1,V1 holds f | (im (f |^ n)) is linear-transformation of (im (f |^ n)),(im (f |^ n))
let f be linear-transformation of V1,V1; ::_thesis: f | (im (f |^ n)) is linear-transformation of (im (f |^ n)),(im (f |^ n))
set IM = im (f |^ n);
 rng (f | (im (f |^ n))) c= the carrier of (im (f |^ n))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (f | (im (f |^ n))) or y in the carrier of (im (f |^ n)) )
assume  y in rng (f | (im (f |^ n))) ; ::_thesis: y in the carrier of (im (f |^ n))
then consider x being set  such that
A1: x in dom (f | (im (f |^ n))) and
A2: (f | (im (f |^ n))) . x = y by FUNCT_1:def_3;
 x in the carrier of (im (f |^ n)) by A1, FUNCT_2:def_1;
then A3: x in im (f |^ n) by STRUCT_0:def_5;
then  x in V1 by VECTSP_4:9;
then reconsider v = x as Vector of V1 by STRUCT_0:def_5;
consider w being Vector of V1 such that
A4: (f |^ n) . w = v by A3, RANKNULL:13;
A5: the carrier of V1 = dom (f |^ 1) by FUNCT_2:def_1;
A6: the carrier of V1 = dom (f |^ n) by FUNCT_2:def_1;
y = f . x by A1, A2, FUNCT_1:47
.= (f * (f |^ n)) . w by A4, A6, FUNCT_1:13
.= ((f |^ 1) * (f |^ n)) . w by Th19
.= (f |^ (1 + n)) . w by Th20
.= ((f |^ n) * (f |^ 1)) . w by Th20
.= (f |^ n) . ((f |^ 1) . w) by A5, FUNCT_1:13 ;
then  y in im (f |^ n) by RANKNULL:13;
hence  y in the carrier of (im (f |^ n)) by STRUCT_0:def_5; ::_thesis: verum
end;
hence  f | (im (f |^ n)) is linear-transformation of (im (f |^ n)),(im (f |^ n)) by Lm1, FUNCT_2:6; ::_thesis: verum
end;

theorem :: VECTSP11:33
for n being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K holds f | (im ((f + (L * (id V1))) |^ n)) is linear-transformation of (im ((f + (L * (id V1))) |^ n)),(im ((f + (L * (id V1))) |^ n))
proof
let n be Nat; ::_thesis: for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K holds f | (im ((f + (L * (id V1))) |^ n)) is linear-transformation of (im ((f + (L * (id V1))) |^ n)),(im ((f + (L * (id V1))) |^ n))
let K be Field; ::_thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K holds f | (im ((f + (L * (id V1))) |^ n)) is linear-transformation of (im ((f + (L * (id V1))) |^ n)),(im ((f + (L * (id V1))) |^ n))
let V1 be VectSp of K; ::_thesis: for f being linear-transformation of V1,V1
for L being Scalar of K holds f | (im ((f + (L * (id V1))) |^ n)) is linear-transformation of (im ((f + (L * (id V1))) |^ n)),(im ((f + (L * (id V1))) |^ n))
let f be linear-transformation of V1,V1; ::_thesis: for L being Scalar of K holds f | (im ((f + (L * (id V1))) |^ n)) is linear-transformation of (im ((f + (L * (id V1))) |^ n)),(im ((f + (L * (id V1))) |^ n))
let L be Scalar of K; ::_thesis: f | (im ((f + (L * (id V1))) |^ n)) is linear-transformation of (im ((f + (L * (id V1))) |^ n)),(im ((f + (L * (id V1))) |^ n))
set fid = f + (L * (id V1));
set IM = im ((f + (L * (id V1))) |^ n);
reconsider fidI = (f + (L * (id V1))) | (im ((f + (L * (id V1))) |^ n)) as linear-transformation of (im ((f + (L * (id V1))) |^ n)),(im ((f + (L * (id V1))) |^ n)) by Th32;
 rng (f | (im ((f + (L * (id V1))) |^ n))) c= the carrier of (im ((f + (L * (id V1))) |^ n))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (f | (im ((f + (L * (id V1))) |^ n))) or y in the carrier of (im ((f + (L * (id V1))) |^ n)) )
assume  y in rng (f | (im ((f + (L * (id V1))) |^ n))) ; ::_thesis: y in the carrier of (im ((f + (L * (id V1))) |^ n))
then consider x being set  such that
A1: x in dom (f | (im ((f + (L * (id V1))) |^ n))) and
A2: (f | (im ((f + (L * (id V1))) |^ n))) . x = y by FUNCT_1:def_3;
A3: x in the carrier of (im ((f + (L * (id V1))) |^ n)) by A1, FUNCT_2:def_1;
then A4: x in im ((f + (L * (id V1))) |^ n) by STRUCT_0:def_5;
then  x in V1 by VECTSP_4:9;
then reconsider v = x as Vector of V1 by STRUCT_0:def_5;
A5: (f | (im ((f + (L * (id V1))) |^ n))) . v = f . v by A1, FUNCT_1:47;
 dom fidI = the carrier of (im ((f + (L * (id V1))) |^ n)) by FUNCT_2:def_1;
then  ( fidI . v = (f + (L * (id V1))) . v & fidI /. v = fidI . v ) by A3, FUNCT_1:47, PARTFUN1:def_6;
then A6: (f + (L * (id V1))) . v in im ((f + (L * (id V1))) |^ n) by STRUCT_0:def_5;
(f + (L * (id V1))) . v = (f . v) + ((L * (id V1)) . v) by MATRLIN:def_3
.= (f . v) + (L * ((id V1) . v)) by MATRLIN:def_4
.= (f . v) + (L * v) by FUNCT_1:18 ;
then A7: ((f + (L * (id V1))) . v) + ((- L) * v) = (f . v) + ((L * v) + ((- L) * v)) by RLVECT_1:def_3
.= (f . v) + ((L + (- L)) * v) by VECTSP_1:def_15
.= (f . v) + ((0. K) * v) by VECTSP_1:16
.= (f . v) + (0. V1) by VECTSP_1:14
.= f . v by RLVECT_1:def_4 ;
 (- L) * v in im ((f + (L * (id V1))) |^ n) by A4, VECTSP_4:21;
then  f . v in im ((f + (L * (id V1))) |^ n) by A7, A6, VECTSP_4:20;
hence  y in the carrier of (im ((f + (L * (id V1))) |^ n)) by A2, A5, STRUCT_0:def_5; ::_thesis: verum
end;
hence  f | (im ((f + (L * (id V1))) |^ n)) is linear-transformation of (im ((f + (L * (id V1))) |^ n)),(im ((f + (L * (id V1))) |^ n)) by Lm1, FUNCT_2:6; ::_thesis: verum
end;

theorem Th34: :: VECTSP11:34
for n being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 st UnionKers f = ker (f |^ n) holds
(ker (f |^ n)) /\ (im (f |^ n)) = (0). V1
proof
let n be Nat; ::_thesis: for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 st UnionKers f = ker (f |^ n) holds
(ker (f |^ n)) /\ (im (f |^ n)) = (0). V1
let K be Field; ::_thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1 st UnionKers f = ker (f |^ n) holds
(ker (f |^ n)) /\ (im (f |^ n)) = (0). V1
let V1 be VectSp of K; ::_thesis: for f being linear-transformation of V1,V1 st UnionKers f = ker (f |^ n) holds
(ker (f |^ n)) /\ (im (f |^ n)) = (0). V1
let f be linear-transformation of V1,V1; ::_thesis: ( UnionKers f = ker (f |^ n) implies (ker (f |^ n)) /\ (im (f |^ n)) = (0). V1 )
set KER = ker (f |^ n);
set IM = im (f |^ n);
assume A1: UnionKers f = ker (f |^ n) ; ::_thesis: (ker (f |^ n)) /\ (im (f |^ n)) = (0). V1
 the carrier of ((ker (f |^ n)) /\ (im (f |^ n))) c= {(0. V1)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((ker (f |^ n)) /\ (im (f |^ n))) or x in {(0. V1)} )
assume  x in the carrier of ((ker (f |^ n)) /\ (im (f |^ n))) ; ::_thesis: x in {(0. V1)}
then A2: x in (ker (f |^ n)) /\ (im (f |^ n)) by STRUCT_0:def_5;
then  x in V1 by VECTSP_4:9;
then reconsider v = x as Vector of V1 by STRUCT_0:def_5;
 v in im (f |^ n) by A2, VECTSP_5:3;
then consider w being Element of V1 such that
A3: (f |^ n) . w = v by RANKNULL:13;
A4: dom (f |^ n) = the carrier of V1 by FUNCT_2:def_1;
 v in ker (f |^ n) by A2, VECTSP_5:3;
then  0. V1 = (f |^ n) . ((f |^ n) . w) by A3, RANKNULL:10
.= ((f |^ n) * (f |^ n)) . w by A4, FUNCT_1:13
.= (f |^ (n + n)) . w by Th20 ;
then  w in ker (f |^ n) by A1, Th24;
then  v = 0. V1 by A3, RANKNULL:10;
hence  x in {(0. V1)} by TARSKI:def_1; ::_thesis: verum
end;
then  the carrier of ((ker (f |^ n)) /\ (im (f |^ n))) = {(0. V1)} by ZFMISC_1:33
.= the carrier of ((0). V1) by VECTSP_4:def_3 ;
hence  (ker (f |^ n)) /\ (im (f |^ n)) = (0). V1 by VECTSP_4:29; ::_thesis: verum
end;

theorem :: VECTSP11:35
for K being Field
for V being finite-dimensional VectSp of K
for f being linear-transformation of V,V
for n being Nat st UnionKers f = ker (f |^ n) holds
V is_the_direct_sum_of ker (f |^ n), im (f |^ n)
proof
let K be Field; ::_thesis: for V being finite-dimensional VectSp of K
for f being linear-transformation of V,V
for n being Nat st UnionKers f = ker (f |^ n) holds
V is_the_direct_sum_of ker (f |^ n), im (f |^ n)
let V be finite-dimensional VectSp of K; ::_thesis: for f being linear-transformation of V,V
for n being Nat st UnionKers f = ker (f |^ n) holds
V is_the_direct_sum_of ker (f |^ n), im (f |^ n)
let f be linear-transformation of V,V; ::_thesis: for n being Nat st UnionKers f = ker (f |^ n) holds
V is_the_direct_sum_of ker (f |^ n), im (f |^ n)
let n be Nat; ::_thesis: ( UnionKers f = ker (f |^ n) implies V is_the_direct_sum_of ker (f |^ n), im (f |^ n) )
set KER = ker (f |^ n);
set IM = im (f |^ n);
A1: dim V = (rank (f |^ n)) + (nullity (f |^ n)) by RANKNULL:44
.= (dim ((im (f |^ n)) + (ker (f |^ n)))) + (dim ((im (f |^ n)) /\ (ker (f |^ n)))) by VECTSP_9:32 ;
assume A2: UnionKers f = ker (f |^ n) ; ::_thesis: V is_the_direct_sum_of ker (f |^ n), im (f |^ n)
then  (Omega). ((im (f |^ n)) /\ (ker (f |^ n))) = (0). V by Th34
.= (0). ((im (f |^ n)) /\ (ker (f |^ n))) by VECTSP_4:36 ;
then  dim ((im (f |^ n)) /\ (ker (f |^ n))) = 0 by VECTSP_9:29;
then  (Omega). V = (Omega). ((im (f |^ n)) + (ker (f |^ n))) by A1, VECTSP_9:28;
then A3: (ker (f |^ n)) + (im (f |^ n)) = (Omega). V by VECTSP_5:5;
 (ker (f |^ n)) /\ (im (f |^ n)) = (0). V by A2, Th34;
hence  V is_the_direct_sum_of ker (f |^ n), im (f |^ n) by A3, VECTSP_5:def_4; ::_thesis: verum
end;

theorem Th36: :: VECTSP11:36
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for I being Linear_Compl of UnionKers f holds f | I is one-to-one
proof
let K be Field; ::_thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1
for I being Linear_Compl of UnionKers f holds f | I is one-to-one
let V1 be VectSp of K; ::_thesis: for f being linear-transformation of V1,V1
for I being Linear_Compl of UnionKers f holds f | I is one-to-one
let f be linear-transformation of V1,V1; ::_thesis: for I being Linear_Compl of UnionKers f holds f | I is one-to-one
let I be Linear_Compl of UnionKers f; ::_thesis: f | I is one-to-one
set fI = f | I;
set U = UnionKers f;
 the carrier of (ker (f | I)) c= {(0. I)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (ker (f | I)) or x in {(0. I)} )
assume  x in the carrier of (ker (f | I)) ; ::_thesis: x in {(0. I)}
then A1: x in ker (f | I) by STRUCT_0:def_5;
then A2: x in I by VECTSP_4:9;
then reconsider v = x as Vector of I by STRUCT_0:def_5;
reconsider w = v as Vector of V1 by VECTSP_4:10;
0. I = 0. V1 by VECTSP_4:11
.= (f | I) . v by A1, RANKNULL:10
.= f . v by FUNCT_1:49 ;
then (f |^ 1) . w = 0. I by Th19
.= 0. V1 by VECTSP_4:11 ;
then  v in UnionKers f by Th24;
then  ( (UnionKers f) /\ I = (0). V1 & v in (UnionKers f) /\ I ) by A2, VECTSP_5:3, VECTSP_5:40;
then  v in the carrier of ((0). V1) by STRUCT_0:def_5;
then  v in {(0. V1)} by VECTSP_4:def_3;
then v = 0. V1 by TARSKI:def_1
.= 0. I by VECTSP_4:11 ;
hence  x in {(0. I)} by TARSKI:def_1; ::_thesis: verum
end;
then  the carrier of (ker (f | I)) = {(0. I)} by ZFMISC_1:33
.= the carrier of ((0). I) by VECTSP_4:def_3 ;
then  ker (f | I) = (0). I by VECTSP_4:29;
hence  f | I is one-to-one by MATRLIN2:43; ::_thesis: verum
end;

theorem Th37: :: VECTSP11:37
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K
for I being Linear_Compl of UnionKers (f + ((- L) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
for v being Vector of I st fI . v = L * v holds
v = 0. V1
proof
let K be Field; ::_thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K
for I being Linear_Compl of UnionKers (f + ((- L) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
for v being Vector of I st fI . v = L * v holds
v = 0. V1
let V1 be VectSp of K; ::_thesis: for f being linear-transformation of V1,V1
for L being Scalar of K
for I being Linear_Compl of UnionKers (f + ((- L) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
for v being Vector of I st fI . v = L * v holds
v = 0. V1
let f be linear-transformation of V1,V1; ::_thesis: for L being Scalar of K
for I being Linear_Compl of UnionKers (f + ((- L) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
for v being Vector of I st fI . v = L * v holds
v = 0. V1
let L be Scalar of K; ::_thesis: for I being Linear_Compl of UnionKers (f + ((- L) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
for v being Vector of I st fI . v = L * v holds
v = 0. V1
set V = V1;
set fi = f + ((- L) * (id V1));
let I be Linear_Compl of UnionKers (f + ((- L) * (id V1))); ::_thesis: for fI being linear-transformation of I,I st fI = f | I holds
for v being Vector of I st fI . v = L * v holds
v = 0. V1
let fI be linear-transformation of I,I; ::_thesis: ( fI = f | I implies for v being Vector of I st fI . v = L * v holds
v = 0. V1 )
assume A1: fI = f | I ; ::_thesis: for v being Vector of I st fI . v = L * v holds
v = 0. V1
let v be Vector of I; ::_thesis: ( fI . v = L * v implies v = 0. V1 )
assume A2: fI . v = L * v ; ::_thesis: v = 0. V1
reconsider v1 = v as Vector of V1 by VECTSP_4:10;
A3: f . v = fI . v by A1, FUNCT_1:49
.= L * v1 by A2, VECTSP_4:14 ;
((f + ((- L) * (id V1))) | I) . v1 = (f + ((- L) * (id V1))) . v1 by FUNCT_1:49
.= (f . v1) + (((- L) * (id V1)) . v1) by MATRLIN:def_3
.= (f . v1) + ((- L) * ((id V1) . v1)) by MATRLIN:def_4
.= (L * v1) + ((- L) * v1) by A3, FUNCT_1:18
.= (L + (- L)) * v1 by VECTSP_1:def_15
.= (0. K) * v1 by VECTSP_1:19
.= 0. V1 by VECTSP_1:14 ;
then A4: v1 in ker ((f + ((- L) * (id V1))) | I) by RANKNULL:10;
 (f + ((- L) * (id V1))) | I is one-to-one by Th36;
then  ker ((f + ((- L) * (id V1))) | I) = (0). I by MATRLIN2:43;
hence v = 0. I by A4, VECTSP_4:35
.= 0. V1 by VECTSP_4:11 ;
::_thesis: verum
end;

Lm3:  for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for a, b being Scalar of K holds (a * b) * f = a * (b * f)
proof
let K be Field; ::_thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1
for a, b being Scalar of K holds (a * b) * f = a * (b * f)
let V1 be VectSp of K; ::_thesis: for f being linear-transformation of V1,V1
for a, b being Scalar of K holds (a * b) * f = a * (b * f)
let f be linear-transformation of V1,V1; ::_thesis: for a, b being Scalar of K holds (a * b) * f = a * (b * f)
let a, b be Scalar of K; ::_thesis: (a * b) * f = a * (b * f)
A1: now__::_thesis:_for_x_being_set_st_x_in_dom_((a_*_b)_*_f)_holds_
((a_*_b)_*_f)_._x_=_(a_*_(b_*_f))_._x
let x be set ; ::_thesis: ( x in dom ((a * b) * f) implies ((a * b) * f) . x = (a * (b * f)) . x )
assume  x in dom ((a * b) * f) ; ::_thesis: ((a * b) * f) . x = (a * (b * f)) . x
then reconsider v = x as Element of V1 by FUNCT_2:def_1;
thus ((a * b) * f) . x = (a * b) * (f . v) by MATRLIN:def_4
.= a * (b * (f . v)) by VECTSP_1:def_16
.= a * ((b * f) . v) by MATRLIN:def_4
.= (a * (b * f)) . x by MATRLIN:def_4 ; ::_thesis: verum
end;
 ( dom ((a * b) * f) = [#] V1 & dom (a * (b * f)) = [#] V1 ) by FUNCT_2:def_1;
hence  (a * b) * f = a * (b * f) by A1, FUNCT_1:2; ::_thesis: verum
end;

Lm4:  for K being Field
for V1 being VectSp of K
for L being Scalar of K
for f, g being Function of V1,V1 holds L * (f * g) = (L * f) * g
proof
let K be Field; ::_thesis: for V1 being VectSp of K
for L being Scalar of K
for f, g being Function of V1,V1 holds L * (f * g) = (L * f) * g
let V1 be VectSp of K; ::_thesis: for L being Scalar of K
for f, g being Function of V1,V1 holds L * (f * g) = (L * f) * g
let L be Scalar of K; ::_thesis: for f, g being Function of V1,V1 holds L * (f * g) = (L * f) * g
let f, g be Function of V1,V1; ::_thesis: L * (f * g) = (L * f) * g
A1: dom ((L * f) * g) = [#] V1 by FUNCT_2:def_1;
A2: dom g = [#] V1 by FUNCT_2:def_1;
A3: now__::_thesis:_for_x_being_set_st_x_in_dom_(L_*_(f_*_g))_holds_
(L_*_(f_*_g))_._x_=_((L_*_f)_*_g)_._x
let x be set ; ::_thesis: ( x in dom (L * (f * g)) implies (L * (f * g)) . x = ((L * f) * g) . x )
assume  x in dom (L * (f * g)) ; ::_thesis: (L * (f * g)) . x = ((L * f) * g) . x
then reconsider v = x as Element of V1 by FUNCT_2:def_1;
thus (L * (f * g)) . x = L * ((f * g) . v) by MATRLIN:def_4
.= L * (f . (g . v)) by A2, FUNCT_1:13
.= (L * f) . (g . v) by MATRLIN:def_4
.= ((L * f) * g) . x by A1, FUNCT_1:12 ; ::_thesis: verum
end;
 dom (L * (f * g)) = [#] V1 by FUNCT_2:def_1;
hence  L * (f * g) = (L * f) * g by A1, A3, FUNCT_1:2; ::_thesis: verum
end;

Lm5:  for K being Field
for V1 being VectSp of K
for L being Scalar of K
for f, g being Function of V1,V1 st f is additive & f is homogeneous holds
L * (f * g) = f * (L * g)
proof
let K be Field; ::_thesis: for V1 being VectSp of K
for L being Scalar of K
for f, g being Function of V1,V1 st f is additive & f is homogeneous holds
L * (f * g) = f * (L * g)
let V1 be VectSp of K; ::_thesis: for L being Scalar of K
for f, g being Function of V1,V1 st f is additive & f is homogeneous holds
L * (f * g) = f * (L * g)
let L be Scalar of K; ::_thesis: for f, g being Function of V1,V1 st f is additive & f is homogeneous holds
L * (f * g) = f * (L * g)
let f, g be Function of V1,V1; ::_thesis: ( f is additive & f is homogeneous implies L * (f * g) = f * (L * g) )
assume A1: ( f is additive & f is homogeneous ) ; ::_thesis: L * (f * g) = f * (L * g)
A2: dom (f * (L * g)) = [#] V1 by FUNCT_2:def_1;
A3: dom g = [#] V1 by FUNCT_2:def_1;
A4: now__::_thesis:_for_x_being_set_st_x_in_dom_(L_*_(f_*_g))_holds_
(L_*_(f_*_g))_._x_=_(f_*_(L_*_g))_._x
let x be set ; ::_thesis: ( x in dom (L * (f * g)) implies (L * (f * g)) . x = (f * (L * g)) . x )
assume  x in dom (L * (f * g)) ; ::_thesis: (L * (f * g)) . x = (f * (L * g)) . x
then reconsider v = x as Element of V1 by FUNCT_2:def_1;
thus (L * (f * g)) . x = L * ((f * g) . v) by MATRLIN:def_4
.= L * (f . (g . v)) by A3, FUNCT_1:13
.= f . (L * (g . v)) by A1, MOD_2:def_2
.= f . ((L * g) . v) by MATRLIN:def_4
.= (f * (L * g)) . x by A2, FUNCT_1:12 ; ::_thesis: verum
end;
 dom (L * (f * g)) = [#] V1 by FUNCT_2:def_1;
hence  L * (f * g) = f * (L * g) by A2, A4, FUNCT_1:2; ::_thesis: verum
end;

Lm6:  for K being Field
for V1 being VectSp of K
for f1, f2, g being Function of V1,V1 holds (f1 + f2) * g = (f1 * g) + (f2 * g)
proof
let K be Field; ::_thesis: for V1 being VectSp of K
for f1, f2, g being Function of V1,V1 holds (f1 + f2) * g = (f1 * g) + (f2 * g)
let V1 be VectSp of K; ::_thesis: for f1, f2, g being Function of V1,V1 holds (f1 + f2) * g = (f1 * g) + (f2 * g)
let f1, f2, g be Function of V1,V1; ::_thesis: (f1 + f2) * g = (f1 * g) + (f2 * g)
A1: dom g = [#] V1 by FUNCT_2:def_1;
A2: dom ((f1 + f2) * g) = [#] V1 by FUNCT_2:def_1;
A3: now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_
((f1_+_f2)_*_g)_._x_=_((f1_*_g)_+_(f2_*_g))_._x
let x be set ; ::_thesis: ( x in dom g implies ((f1 + f2) * g) . x = ((f1 * g) + (f2 * g)) . x )
assume  x in dom g ; ::_thesis: ((f1 + f2) * g) . x = ((f1 * g) + (f2 * g)) . x
then reconsider v = x as Element of V1 by FUNCT_2:def_1;
thus ((f1 + f2) * g) . x = (f1 + f2) . (g . v) by A2, FUNCT_1:12
.= (f1 . (g . v)) + (f2 . (g . v)) by MATRLIN:def_3
.= ((f1 * g) . v) + (f2 . (g . v)) by A1, FUNCT_1:13
.= ((f1 * g) . v) + ((f2 * g) . v) by A1, FUNCT_1:13
.= ((f1 * g) + (f2 * g)) . x by MATRLIN:def_3 ; ::_thesis: verum
end;
 dom ((f1 * g) + (f2 * g)) = [#] V1 by FUNCT_2:def_1;
hence  (f1 + f2) * g = (f1 * g) + (f2 * g) by A2, A1, A3, FUNCT_1:2; ::_thesis: verum
end;

Lm7:  for K being Field
for V1 being VectSp of K
for f1, f2, g being Function of V1,V1 st g is additive & g is homogeneous holds
g * (f1 + f2) = (g * f1) + (g * f2)
proof
let K be Field; ::_thesis: for V1 being VectSp of K
for f1, f2, g being Function of V1,V1 st g is additive & g is homogeneous holds
g * (f1 + f2) = (g * f1) + (g * f2)
let V1 be VectSp of K; ::_thesis: for f1, f2, g being Function of V1,V1 st g is additive & g is homogeneous holds
g * (f1 + f2) = (g * f1) + (g * f2)
let f1, f2, g be Function of V1,V1; ::_thesis: ( g is additive & g is homogeneous implies g * (f1 + f2) = (g * f1) + (g * f2) )
assume A1: ( g is additive & g is homogeneous ) ; ::_thesis: g * (f1 + f2) = (g * f1) + (g * f2)
A2: dom (g * (f1 + f2)) = [#] V1 by FUNCT_2:def_1;
A3: dom f2 = [#] V1 by FUNCT_2:def_1;
A4: dom f1 = [#] V1 by FUNCT_2:def_1;
A5: now__::_thesis:_for_x_being_set_st_x_in_dom_(g_*_(f1_+_f2))_holds_
(g_*_(f1_+_f2))_._x_=_((g_*_f1)_+_(g_*_f2))_._x
let x be set ; ::_thesis: ( x in dom (g * (f1 + f2)) implies (g * (f1 + f2)) . x = ((g * f1) + (g * f2)) . x )
assume  x in dom (g * (f1 + f2)) ; ::_thesis: (g * (f1 + f2)) . x = ((g * f1) + (g * f2)) . x
then reconsider v = x as Element of V1 by FUNCT_2:def_1;
thus (g * (f1 + f2)) . x = g . ((f1 + f2) . v) by A2, FUNCT_1:12
.= g . ((f1 . v) + (f2 . v)) by MATRLIN:def_3
.= (g . (f1 . v)) + (g . (f2 . v)) by A1, VECTSP_1:def_20
.= ((g * f1) . v) + (g . (f2 . v)) by A4, FUNCT_1:13
.= ((g * f1) . v) + ((g * f2) . v) by A3, FUNCT_1:13
.= ((g * f1) + (g * f2)) . x by MATRLIN:def_3 ; ::_thesis: verum
end;
 dom ((g * f1) + (g * f2)) = [#] V1 by FUNCT_2:def_1;
hence  g * (f1 + f2) = (g * f1) + (g * f2) by A2, A5, FUNCT_1:2; ::_thesis: verum
end;

Lm8:  for K being Field
for V1 being VectSp of K
for f1, f2, f3 being Function of V1,V1 holds (f1 + f2) + f3 = f1 + (f2 + f3)
proof
let K be Field; ::_thesis: for V1 being VectSp of K
for f1, f2, f3 being Function of V1,V1 holds (f1 + f2) + f3 = f1 + (f2 + f3)
let V1 be VectSp of K; ::_thesis: for f1, f2, f3 being Function of V1,V1 holds (f1 + f2) + f3 = f1 + (f2 + f3)
let f1, f2, f3 be Function of V1,V1; ::_thesis: (f1 + f2) + f3 = f1 + (f2 + f3)
A1: now__::_thesis:_for_x_being_set_st_x_in_dom_((f1_+_f2)_+_f3)_holds_
((f1_+_f2)_+_f3)_._x_=_(f1_+_(f2_+_f3))_._x
let x be set ; ::_thesis: ( x in dom ((f1 + f2) + f3) implies ((f1 + f2) + f3) . x = (f1 + (f2 + f3)) . x )
assume  x in dom ((f1 + f2) + f3) ; ::_thesis: ((f1 + f2) + f3) . x = (f1 + (f2 + f3)) . x
then reconsider v = x as Element of V1 by FUNCT_2:def_1;
thus ((f1 + f2) + f3) . x = ((f1 + f2) . v) + (f3 . v) by MATRLIN:def_3
.= ((f1 . v) + (f2 . v)) + (f3 . v) by MATRLIN:def_3
.= (f1 . v) + ((f2 . v) + (f3 . v)) by RLVECT_1:def_3
.= (f1 . v) + ((f2 + f3) . v) by MATRLIN:def_3
.= (f1 + (f2 + f3)) . x by MATRLIN:def_3 ; ::_thesis: verum
end;
 ( dom ((f1 + f2) + f3) = [#] V1 & dom (f1 + (f2 + f3)) = [#] V1 ) by FUNCT_2:def_1;
hence  (f1 + f2) + f3 = f1 + (f2 + f3) by A1, FUNCT_1:2; ::_thesis: verum
end;

Lm9:  for n being Nat
for K being Field
for V1 being VectSp of K
for L being Scalar of K holds (L * (id V1)) |^ n = ((power K) . (L,n)) * (id V1)
proof
let n be Nat; ::_thesis: for K being Field
for V1 being VectSp of K
for L being Scalar of K holds (L * (id V1)) |^ n = ((power K) . (L,n)) * (id V1)
let K be Field; ::_thesis: for V1 being VectSp of K
for L being Scalar of K holds (L * (id V1)) |^ n = ((power K) . (L,n)) * (id V1)
let V1 be VectSp of K; ::_thesis: for L being Scalar of K holds (L * (id V1)) |^ n = ((power K) . (L,n)) * (id V1)
let L be Scalar of K; ::_thesis: (L * (id V1)) |^ n = ((power K) . (L,n)) * (id V1)
defpred S1[ Nat] means (L * (id V1)) |^ $1 = ((power K) . (L,$1)) * (id V1);
A1: ( dom (id V1) = [#] V1 & dom ((1_ K) * (id V1)) = [#] V1 ) by FUNCT_2:def_1;
A2: now__::_thesis:_for_x_being_set_st_x_in_[#]_V1_holds_
(id_V1)_._x_=_((1__K)_*_(id_V1))_._x
let x be set ; ::_thesis: ( x in [#] V1 implies (id V1) . x = ((1_ K) * (id V1)) . x )
assume  x in [#] V1 ; ::_thesis: (id V1) . x = ((1_ K) * (id V1)) . x
then reconsider v = x as Vector of V1 ;
 ( (id V1) . x = v & (1_ K) * v = v ) by FUNCT_1:18, VECTSP_1:def_17;
hence  (id V1) . x = ((1_ K) * (id V1)) . x by MATRLIN:def_4; ::_thesis: verum
end;
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; ::_thesis: S1[n + 1]
A5: n in NAT by ORDINAL1:def_12;
thus (L * (id V1)) |^ (n + 1) = ((L * (id V1)) |^ 1) * (((power K) . (L,n)) * (id V1)) by A4, Th20
.= (L * (id V1)) * (((power K) . (L,n)) * (id V1)) by Th19
.= ((power K) . (L,n)) * ((L * (id V1)) * (id V1)) by Lm5
.= ((power K) . (L,n)) * (L * ((id V1) * (id V1))) by Lm4
.= ((power K) . (L,n)) * (L * (id V1)) by SYSREL:12
.= (((power K) . (L,n)) * L) * (id V1) by Lm3
.= ((power K) . (L,(n + 1))) * (id V1) by A5, GROUP_1:def_7 ; ::_thesis: verum
end;
 ( (L * (id V1)) |^ 0 = id V1 & (power K) . (L,0) = 1_ K ) by Th18, GROUP_1:def_7;
then A6: S1[ 0 ] by A1, A2, FUNCT_1:2;
 for n being Nat holds S1[n] from NAT_1:sch_2(A6, A3);
hence  (L * (id V1)) |^ n = ((power K) . (L,n)) * (id V1) ; ::_thesis: verum
end;

Lm10:  for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for a, b being Scalar of K holds (a + b) * f = (a * f) + (b * f)
proof
let K be Field; ::_thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1
for a, b being Scalar of K holds (a + b) * f = (a * f) + (b * f)
let V1 be VectSp of K; ::_thesis: for f being linear-transformation of V1,V1
for a, b being Scalar of K holds (a + b) * f = (a * f) + (b * f)
let f be linear-transformation of V1,V1; ::_thesis: for a, b being Scalar of K holds (a + b) * f = (a * f) + (b * f)
let a, b be Scalar of K; ::_thesis: (a + b) * f = (a * f) + (b * f)
A1: now__::_thesis:_for_x_being_set_st_x_in_dom_((a_+_b)_*_f)_holds_
((a_+_b)_*_f)_._x_=_((a_*_f)_+_(b_*_f))_._x
let x be set ; ::_thesis: ( x in dom ((a + b) * f) implies ((a + b) * f) . x = ((a * f) + (b * f)) . x )
assume  x in dom ((a + b) * f) ; ::_thesis: ((a + b) * f) . x = ((a * f) + (b * f)) . x
then reconsider v = x as Element of V1 by FUNCT_2:def_1;
thus ((a + b) * f) . x = (a + b) * (f . v) by MATRLIN:def_4
.= (a * (f . v)) + (b * (f . v)) by VECTSP_1:def_15
.= ((a * f) . v) + (b * (f . v)) by MATRLIN:def_4
.= ((a * f) . v) + ((b * f) . v) by MATRLIN:def_4
.= ((a * f) + (b * f)) . x by MATRLIN:def_3 ; ::_thesis: verum
end;
 ( dom ((a + b) * f) = [#] V1 & dom ((a * f) + (b * f)) = [#] V1 ) by FUNCT_2:def_1;
hence  (a + b) * f = (a * f) + (b * f) by A1, FUNCT_1:2; ::_thesis: verum
end;

theorem Th38: :: VECTSP11:38
for n being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K st n >= 1 holds
ex h being linear-transformation of V1,V1 st
( (f + (L * (id V1))) |^ n = (f * h) + ((L * (id V1)) |^ n) & ( for i being Nat holds (f |^ i) * h = h * (f |^ i) ) )
proof
let n be Nat; ::_thesis: for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K st n >= 1 holds
ex h being linear-transformation of V1,V1 st
( (f + (L * (id V1))) |^ n = (f * h) + ((L * (id V1)) |^ n) & ( for i being Nat holds (f |^ i) * h = h * (f |^ i) ) )
let K be Field; ::_thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K st n >= 1 holds
ex h being linear-transformation of V1,V1 st
( (f + (L * (id V1))) |^ n = (f * h) + ((L * (id V1)) |^ n) & ( for i being Nat holds (f |^ i) * h = h * (f |^ i) ) )
let V1 be VectSp of K; ::_thesis: for f being linear-transformation of V1,V1
for L being Scalar of K st n >= 1 holds
ex h being linear-transformation of V1,V1 st
( (f + (L * (id V1))) |^ n = (f * h) + ((L * (id V1)) |^ n) & ( for i being Nat holds (f |^ i) * h = h * (f |^ i) ) )
let f be linear-transformation of V1,V1; ::_thesis: for L being Scalar of K st n >= 1 holds
ex h being linear-transformation of V1,V1 st
( (f + (L * (id V1))) |^ n = (f * h) + ((L * (id V1)) |^ n) & ( for i being Nat holds (f |^ i) * h = h * (f |^ i) ) )
let L be Scalar of K; ::_thesis: ( n >= 1 implies ex h being linear-transformation of V1,V1 st
( (f + (L * (id V1))) |^ n = (f * h) + ((L * (id V1)) |^ n) & ( for i being Nat holds (f |^ i) * h = h * (f |^ i) ) ) )
set g = L * (id V1);
defpred S1[ Nat] means  ex h being linear-transformation of V1,V1 st
( (f + (L * (id V1))) |^ $1 = (f * h) + ((L * (id V1)) |^ $1) & ( for i being Nat holds (f |^ i) * h = h * (f |^ i) ) );
A1: for n being Nat st 1 <= n & S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( 1 <= n & S1[n] implies S1[n + 1] )
assume  1 <= n ; ::_thesis: ( not S1[n] or S1[n + 1] )
assume  S1[n] ; ::_thesis: S1[n + 1]
then consider h being linear-transformation of V1,V1 such that
A2: (f + (L * (id V1))) |^ n = (f * h) + ((L * (id V1)) |^ n) and
A3: for i being Nat holds (f |^ i) * h = h * (f |^ i) ;
take H = ((f * h) + ((L * (id V1)) |^ n)) + (L * h); ::_thesis: ( (f + (L * (id V1))) |^ (n + 1) = (f * H) + ((L * (id V1)) |^ (n + 1)) & ( for i being Nat holds (f |^ i) * H = H * (f |^ i) ) )
A4: rng (f * h) c= [#] V1 by RELAT_1:def_19;
thus (f + (L * (id V1))) |^ (n + 1) = ((f + (L * (id V1))) |^ 1) * ((f + (L * (id V1))) |^ n) by Th20
.= (f + (L * (id V1))) * ((f * h) + ((L * (id V1)) |^ n)) by A2, Th19
.= (f * ((f * h) + ((L * (id V1)) |^ n))) + ((L * (id V1)) * ((f * h) + ((L * (id V1)) |^ n))) by Lm6
.= (f * ((f * h) + ((L * (id V1)) |^ n))) + (((L * (id V1)) * (f * h)) + ((L * (id V1)) * ((L * (id V1)) |^ n))) by Lm7
.= ((f * ((f * h) + ((L * (id V1)) |^ n))) + ((L * (id V1)) * (f * h))) + ((L * (id V1)) * ((L * (id V1)) |^ n)) by Lm8
.= ((f * ((f * h) + ((L * (id V1)) |^ n))) + (L * ((id V1) * (f * h)))) + ((L * (id V1)) * ((L * (id V1)) |^ n)) by Lm4
.= ((f * ((f * h) + ((L * (id V1)) |^ n))) + (L * (f * h))) + ((L * (id V1)) * ((L * (id V1)) |^ n)) by A4, RELAT_1:53
.= ((f * ((f * h) + ((L * (id V1)) |^ n))) + (f * (L * h))) + ((L * (id V1)) * ((L * (id V1)) |^ n)) by Lm5
.= (f * H) + ((L * (id V1)) * ((L * (id V1)) |^ n)) by Lm7
.= (f * H) + (((L * (id V1)) |^ 1) * ((L * (id V1)) |^ n)) by Th19
.= (f * H) + ((L * (id V1)) |^ (n + 1)) by Th20 ; ::_thesis: for i being Nat holds (f |^ i) * H = H * (f |^ i)
let i be Nat; ::_thesis: (f |^ i) * H = H * (f |^ i)
A5: (f |^ i) * (f * h) = ((f |^ i) * f) * h by RELAT_1:36
.= ((f |^ i) * (f |^ 1)) * h by Th19
.= (f |^ (i + 1)) * h by Th20
.= h * (f |^ (i + 1)) by A3
.= h * ((f |^ 1) * (f |^ i)) by Th20
.= (h * (f |^ 1)) * (f |^ i) by RELAT_1:36
.= ((f |^ 1) * h) * (f |^ i) by A3
.= (f * h) * (f |^ i) by Th19 ;
A6: (f |^ i) * ((L * (id V1)) |^ n) = (f |^ i) * (((power K) . (L,n)) * (id V1)) by Lm9
.= ((power K) . (L,n)) * ((f |^ i) * (id V1)) by Lm5
.= ((power K) . (L,n)) * ((f |^ i) * (f |^ 0)) by Th18
.= ((power K) . (L,n)) * (f |^ (i + 0)) by Th20
.= ((power K) . (L,n)) * ((f |^ 0) * (f |^ i)) by Th20
.= ((power K) . (L,n)) * ((id V1) * (f |^ i)) by Th18
.= (((power K) . (L,n)) * (id V1)) * (f |^ i) by Lm4
.= ((L * (id V1)) |^ n) * (f |^ i) by Lm9 ;
(f |^ i) * (L * h) = L * ((f |^ i) * h) by Lm5
.= L * (h * (f |^ i)) by A3
.= (L * h) * (f |^ i) by Lm4 ;
hence (f |^ i) * H = ((f |^ i) * ((f * h) + ((L * (id V1)) |^ n))) + ((L * h) * (f |^ i)) by Lm7
.= (((f * h) * (f |^ i)) + (((L * (id V1)) |^ n) * (f |^ i))) + ((L * h) * (f |^ i)) by A5, A6, Lm7
.= (((f * h) + ((L * (id V1)) |^ n)) * (f |^ i)) + ((L * h) * (f |^ i)) by Lm6
.= H * (f |^ i) by Lm6 ;
::_thesis: verum
end;
A7: S1[1]
proof
take h = id V1; ::_thesis: ( (f + (L * (id V1))) |^ 1 = (f * h) + ((L * (id V1)) |^ 1) & ( for i being Nat holds (f |^ i) * h = h * (f |^ i) ) )
thus (f + (L * (id V1))) |^ 1 = f + (L * (id V1)) by Th19
.= (f |^ (1 + 0)) + (L * (id V1)) by Th19
.= ((f |^ 1) * (f |^ 0)) + (L * (id V1)) by Th20
.= ((f |^ 1) * h) + (L * (id V1)) by Th18
.= (f * h) + (L * (id V1)) by Th19
.= (f * h) + ((L * (id V1)) |^ 1) by Th19 ; ::_thesis: for i being Nat holds (f |^ i) * h = h * (f |^ i)
let i be Nat; ::_thesis: (f |^ i) * h = h * (f |^ i)
thus (f |^ i) * h = (f |^ i) * (f |^ 0) by Th18
.= f |^ (i + 0) by Th20
.= (f |^ 0) * (f |^ i) by Th20
.= h * (f |^ i) by Th18 ; ::_thesis: verum
end;
 for n being Nat st 1 <= n holds
S1[n] from NAT_1:sch_8(A7, A1);
hence  ( n >= 1 implies ex h being linear-transformation of V1,V1 st
( (f + (L * (id V1))) |^ n = (f * h) + ((L * (id V1)) |^ n) & ( for i being Nat holds (f |^ i) * h = h * (f |^ i) ) ) ) ; ::_thesis: verum
end;

theorem :: VECTSP11:39
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L1, L2 being Scalar of K st f is with_eigenvalues & L1 <> L2 & L2 is eigenvalue of f holds
for I being Linear_Compl of UnionKers (f + ((- L1) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
( fI is with_eigenvalues & L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I )
proof
let K be Field; ::_thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L1, L2 being Scalar of K st f is with_eigenvalues & L1 <> L2 & L2 is eigenvalue of f holds
for I being Linear_Compl of UnionKers (f + ((- L1) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
( fI is with_eigenvalues & L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I )
let V1 be VectSp of K; ::_thesis: for f being linear-transformation of V1,V1
for L1, L2 being Scalar of K st f is with_eigenvalues & L1 <> L2 & L2 is eigenvalue of f holds
for I being Linear_Compl of UnionKers (f + ((- L1) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
( fI is with_eigenvalues & L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I )
let f be linear-transformation of V1,V1; ::_thesis: for L1, L2 being Scalar of K st f is with_eigenvalues & L1 <> L2 & L2 is eigenvalue of f holds
for I being Linear_Compl of UnionKers (f + ((- L1) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
( fI is with_eigenvalues & L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I )
let L1, L2 be Scalar of K; ::_thesis: ( f is with_eigenvalues & L1 <> L2 & L2 is eigenvalue of f implies for I being Linear_Compl of UnionKers (f + ((- L1) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
( fI is with_eigenvalues & L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I ) )
assume that
A1: f is with_eigenvalues and
A2: L1 <> L2 and
A3: L2 is eigenvalue of f ; ::_thesis: for I being Linear_Compl of UnionKers (f + ((- L1) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
( fI is with_eigenvalues & L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I )
set V = V1;
consider v being Vector of V1 such that
A4: v <> 0. V1 and
A5: f . v = L2 * v by A1, A3, Def2;
set f1 = f + ((- L1) * (id V1));
set U = UnionKers (f + ((- L1) * (id V1)));
reconsider fU = f | (UnionKers (f + ((- L1) * (id V1)))) as linear-transformation of (UnionKers (f + ((- L1) * (id V1)))),(UnionKers (f + ((- L1) * (id V1)))) by Th31;
set f2 = f + ((- L2) * (id V1));
let I be Linear_Compl of UnionKers (f + ((- L1) * (id V1))); ::_thesis: for fI being linear-transformation of I,I st fI = f | I holds
( fI is with_eigenvalues & L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I )
let fI be linear-transformation of I,I; ::_thesis: ( fI = f | I implies ( fI is with_eigenvalues & L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I ) )
assume A6: fI = f | I ; ::_thesis: ( fI is with_eigenvalues & L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I )
A7: now__::_thesis:_for_v_being_Vector_of_V1_st_v_in_UnionKers_(f_+_((-_L2)_*_(id_V1)))_holds_
v_is_Vector_of_I
let v be Vector of V1; ::_thesis: ( v in UnionKers (f + ((- L2) * (id V1))) implies v is Vector of I )
assume  v in UnionKers (f + ((- L2) * (id V1))) ; ::_thesis: v is Vector of I
then consider m being Nat such that
A8: ((f + ((- L2) * (id V1))) |^ m) . v = 0. V1 by Th24;
set v1 = v |-- (I,(UnionKers (f + ((- L1) * (id V1)))));
set i1 = (v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `1 ;
set u1 = (v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2 ;
A9: V1 is_the_direct_sum_of I, UnionKers (f + ((- L1) * (id V1))) by VECTSP_5:def_5;
then A10: v = ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `1) + ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2) by VECTSP_5:def_6;
defpred S1[ Nat] means ((f + ((- L2) * (id V1))) |^ $1) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2) = 0. V1;
defpred S2[ Nat] means  for W being Subspace of V1 st ( W = I or W = UnionKers (f + ((- L1) * (id V1))) ) holds
for w being Vector of V1 st w in W holds
((f + ((- L2) * (id V1))) |^ $1) . w in W;
set L21 = L2 - L1;
set f21 = (f + ((- L2) * (id V1))) + ((L2 - L1) * (id V1));
A11: ( 0. V1 in I & 0. V1 in UnionKers (f + ((- L1) * (id V1))) ) by VECTSP_4:17;
A12: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A13: S2[n] ; ::_thesis: S2[n + 1]
let W be Subspace of V1; ::_thesis: ( ( W = I or W = UnionKers (f + ((- L1) * (id V1))) ) implies for w being Vector of V1 st w in W holds
((f + ((- L2) * (id V1))) |^ (n + 1)) . w in W )
assume A14: ( W = I or W = UnionKers (f + ((- L1) * (id V1))) ) ; ::_thesis: for w being Vector of V1 st w in W holds
((f + ((- L2) * (id V1))) |^ (n + 1)) . w in W
let w be Vector of V1; ::_thesis: ( w in W implies ((f + ((- L2) * (id V1))) |^ (n + 1)) . w in W )
assume A15: w in W ; ::_thesis: ((f + ((- L2) * (id V1))) |^ (n + 1)) . w in W
set fnw = ((f + ((- L2) * (id V1))) |^ n) . w;
A16: ((f + ((- L2) * (id V1))) |^ n) . w in W by A13, A14, A15;
A17: now__::_thesis:_f_._(((f_+_((-_L2)_*_(id_V1)))_|^_n)_._w)_in_W
percases ( W = I or W = UnionKers (f + ((- L1) * (id V1))) ) by A14;
supposeA18: W = I ; ::_thesis: f . (((f + ((- L2) * (id V1))) |^ n) . w) in W
then reconsider F = ((f + ((- L2) * (id V1))) |^ n) . w as Vector of I by A16, STRUCT_0:def_5;
 f . (((f + ((- L2) * (id V1))) |^ n) . w) = fI . F by A6, FUNCT_1:49;
hence  f . (((f + ((- L2) * (id V1))) |^ n) . w) in W by A18, STRUCT_0:def_5; ::_thesis: verum
end;
supposeA19: W = UnionKers (f + ((- L1) * (id V1))) ; ::_thesis: f . (((f + ((- L2) * (id V1))) |^ n) . w) in W
then reconsider F = ((f + ((- L2) * (id V1))) |^ n) . w as Vector of (UnionKers (f + ((- L1) * (id V1)))) by A16, STRUCT_0:def_5;
 f . (((f + ((- L2) * (id V1))) |^ n) . w) = fU . F by FUNCT_1:49;
hence  f . (((f + ((- L2) * (id V1))) |^ n) . w) in W by A19, STRUCT_0:def_5; ::_thesis: verum
end;
end;
end;
((- L2) * (id V1)) . (((f + ((- L2) * (id V1))) |^ n) . w) = (- L2) * ((id V1) . (((f + ((- L2) * (id V1))) |^ n) . w)) by MATRLIN:def_4
.= (- L2) * (((f + ((- L2) * (id V1))) |^ n) . w) by FUNCT_1:18 ;
then A20: ((- L2) * (id V1)) . (((f + ((- L2) * (id V1))) |^ n) . w) in W by A16, VECTSP_4:21;
A21: dom ((f + ((- L2) * (id V1))) |^ n) = [#] V1 by FUNCT_2:def_1;
((f + ((- L2) * (id V1))) |^ (n + 1)) . w = (((f + ((- L2) * (id V1))) |^ 1) * ((f + ((- L2) * (id V1))) |^ n)) . w by Th20
.= ((f + ((- L2) * (id V1))) |^ 1) . (((f + ((- L2) * (id V1))) |^ n) . w) by A21, FUNCT_1:13
.= (f + ((- L2) * (id V1))) . (((f + ((- L2) * (id V1))) |^ n) . w) by Th19
.= (f . (((f + ((- L2) * (id V1))) |^ n) . w)) + (((- L2) * (id V1)) . (((f + ((- L2) * (id V1))) |^ n) . w)) by MATRLIN:def_3 ;
hence  ((f + ((- L2) * (id V1))) |^ (n + 1)) . w in W by A17, A20, VECTSP_4:20; ::_thesis: verum
end;
A22: (0. V1) + (0. V1) = 0. V1 by RLVECT_1:def_4
.= (((f + ((- L2) * (id V1))) |^ m) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `1)) + (((f + ((- L2) * (id V1))) |^ m) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2)) by A10, A8, VECTSP_1:def_20 ;
A23: (v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2 in UnionKers (f + ((- L1) * (id V1))) by A9, VECTSP_5:def_6;
then consider n being Nat such that
A24: ((f + ((- L1) * (id V1))) |^ n) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2) = 0. V1 by Th24;
A25: S2[ 0 ]
proof
let W be Subspace of V1; ::_thesis: ( ( W = I or W = UnionKers (f + ((- L1) * (id V1))) ) implies for w being Vector of V1 st w in W holds
((f + ((- L2) * (id V1))) |^ 0) . w in W )
assume  ( W = I or W = UnionKers (f + ((- L1) * (id V1))) ) ; ::_thesis: for w being Vector of V1 st w in W holds
((f + ((- L2) * (id V1))) |^ 0) . w in W
let w be Vector of V1; ::_thesis: ( w in W implies ((f + ((- L2) * (id V1))) |^ 0) . w in W )
assume A26: w in W ; ::_thesis: ((f + ((- L2) * (id V1))) |^ 0) . w in W
((f + ((- L2) * (id V1))) |^ 0) . w = (id V1) . w by Th18
.= w by FUNCT_1:18 ;
hence  ((f + ((- L2) * (id V1))) |^ 0) . w in W by A26; ::_thesis: verum
end;
A27: for n being Nat holds S2[n] from NAT_1:sch_2(A25, A12);
then A28: ((f + ((- L2) * (id V1))) |^ m) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2) in UnionKers (f + ((- L1) * (id V1))) by A23;
A29: (v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `1 in I by A9, VECTSP_5:def_6;
then  ((f + ((- L2) * (id V1))) |^ m) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `1) in I by A27;
then  ((f + ((- L2) * (id V1))) |^ m) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2) = 0. V1 by A9, A28, A11, A22, VECTSP_5:48;
then A30: ex m being Nat st S1[m] ;
consider MIN being Nat such that
A31: S1[MIN] and
A32: for n being Nat st S1[n] holds
MIN <= n from NAT_1:sch_5(A30);
assume A33: v is not Vector of I ; ::_thesis: contradiction
A34: (v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2 <> 0. V1
proof
assume  (v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2 = 0. V1 ; ::_thesis: contradiction
then  v = (v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `1 by A10, RLVECT_1:def_4;
hence  contradiction by A29, A33, STRUCT_0:def_5; ::_thesis: verum
end;
 n <> 0
proof
assume  n = 0 ; ::_thesis: contradiction
then  0. V1 = (id V1) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2) by A24, Th18
.= (v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2 by FUNCT_1:18 ;
hence  contradiction by A34; ::_thesis: verum
end;
then consider h being linear-transformation of V1,V1 such that
A35: ((f + ((- L2) * (id V1))) + ((L2 - L1) * (id V1))) |^ n = ((f + ((- L2) * (id V1))) * h) + (((L2 - L1) * (id V1)) |^ n) and
A36: for i being Nat holds ((f + ((- L2) * (id V1))) |^ i) * h = h * ((f + ((- L2) * (id V1))) |^ i) by Th38, NAT_1:14;
A37: dom (((f + ((- L2) * (id V1))) + ((L2 - L1) * (id V1))) |^ n) = [#] V1 by FUNCT_2:def_1;
 MIN <> 0
proof
assume  MIN = 0 ; ::_thesis: contradiction
then  0. V1 = (id V1) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2) by A31, Th18
.= (v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2 by FUNCT_1:18 ;
hence  contradiction by A34; ::_thesis: verum
end;
then reconsider M1 = MIN - 1 as Element of NAT by NAT_1:20;
A38: ((f + ((- L2) * (id V1))) |^ M1) * ((f + ((- L2) * (id V1))) * h) = (((f + ((- L2) * (id V1))) |^ M1) * (f + ((- L2) * (id V1)))) * h by RELAT_1:36
.= (((f + ((- L2) * (id V1))) |^ M1) * ((f + ((- L2) * (id V1))) |^ 1)) * h by Th19
.= ((f + ((- L2) * (id V1))) |^ (M1 + 1)) * h by Th20
.= h * ((f + ((- L2) * (id V1))) |^ MIN) by A36 ;
 dom (((L2 - L1) * (id V1)) |^ n) = [#] V1 by FUNCT_2:def_1;
then A39: (((f + ((- L2) * (id V1))) |^ M1) * (((L2 - L1) * (id V1)) |^ n)) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2) = ((f + ((- L2) * (id V1))) |^ M1) . ((((L2 - L1) * (id V1)) |^ n) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2)) by FUNCT_1:13
.= ((f + ((- L2) * (id V1))) |^ M1) . ((((power K) . ((L2 - L1),n)) * (id V1)) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2)) by Lm9
.= ((f + ((- L2) * (id V1))) |^ M1) . (((power K) . ((L2 - L1),n)) * ((id V1) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2))) by MATRLIN:def_4
.= ((f + ((- L2) * (id V1))) |^ M1) . (((power K) . ((L2 - L1),n)) * ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2)) by FUNCT_1:18
.= ((power K) . ((L2 - L1),n)) * (((f + ((- L2) * (id V1))) |^ M1) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2)) by MOD_2:def_2 ;
A40: (power K) . ((L2 - L1),n) <> 0. K
proof
assume  0. K = (power K) . ((L2 - L1),n) ; ::_thesis: contradiction
then  0. K = Product (n |-> (L2 - L1)) by MATRIXJ1:5;
then A41: ex k being Element of NAT st
( k in dom (n |-> (L2 - L1)) & (n |-> (L2 - L1)) . k = 0. K ) by FVSUM_1:82;
 dom (n |-> (L2 - L1)) = Seg n by FINSEQ_2:124;
then  L2 - L1 = 0. K by A41, FINSEQ_2:57;
hence  contradiction by A2, VECTSP_1:19; ::_thesis: verum
end;
 dom ((f + ((- L2) * (id V1))) |^ MIN) = [#] V1 by FUNCT_2:def_1;
then A42: (h * ((f + ((- L2) * (id V1))) |^ MIN)) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2) = h . (((f + ((- L2) * (id V1))) |^ MIN) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2)) by FUNCT_1:13
.= 0. V1 by A31, RANKNULL:9 ;
(f + ((- L2) * (id V1))) + ((L2 - L1) * (id V1)) = f + (((- L2) * (id V1)) + ((L2 - L1) * (id V1))) by Lm8
.= f + (((- L2) + (L2 - L1)) * (id V1)) by Lm10
.= f + ((((- L2) + L2) - L1) * (id V1)) by RLVECT_1:def_3
.= f + (((0. K) + (- L1)) * (id V1)) by VECTSP_1:19
.= f + ((- L1) * (id V1)) by RLVECT_1:def_4 ;
then  0. V1 = ((f + ((- L2) * (id V1))) |^ M1) . ((((f + ((- L2) * (id V1))) + ((L2 - L1) * (id V1))) |^ n) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2)) by A24, RANKNULL:9
.= (((f + ((- L2) * (id V1))) |^ M1) * (((f + ((- L2) * (id V1))) * h) + (((L2 - L1) * (id V1)) |^ n))) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2) by A35, A37, FUNCT_1:13
.= ((h * ((f + ((- L2) * (id V1))) |^ MIN)) + (((f + ((- L2) * (id V1))) |^ M1) * (((L2 - L1) * (id V1)) |^ n))) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2) by A38, Lm7
.= (0. V1) + (((power K) . ((L2 - L1),n)) * (((f + ((- L2) * (id V1))) |^ M1) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2))) by A42, A39, MATRLIN:def_3
.= ((power K) . ((L2 - L1),n)) * (((f + ((- L2) * (id V1))) |^ M1) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2)) by RLVECT_1:def_4 ;
then  ((f + ((- L2) * (id V1))) |^ M1) . ((v |-- (I,(UnionKers (f + ((- L1) * (id V1)))))) `2) = 0. V1 by A40, VECTSP_1:15;
then  M1 + 1 <= M1 by A32;
hence  contradiction by NAT_1:13; ::_thesis: verum
end;
 v is eigenvector of f,L2 by A1, A3, A5, Def3;
then  v in ker (f + ((- L2) * (id V1))) by A1, A3, Th17;
then  0. V1 = (f + ((- L2) * (id V1))) . v by RANKNULL:10
.= ((f + ((- L2) * (id V1))) |^ 1) . v by Th19 ;
then  v in UnionKers (f + ((- L2) * (id V1))) by Th24;
then reconsider vI = v as Vector of I by A7;
A43: ( 0. V1 = 0. I & L2 * v = L2 * vI ) by VECTSP_4:11, VECTSP_4:14;
A44: f . v = fI . vI by A6, FUNCT_1:49;
hence A45: fI is with_eigenvalues by A4, A5, A43, Def1; ::_thesis: ( L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I )
 L1 is not eigenvalue of fI
proof
assume  L1 is eigenvalue of fI ; ::_thesis: contradiction
then consider w being Vector of I such that
A46: w <> 0. I and
A47: fI . w = L1 * w by A45, Def2;
 w = 0. V1 by A6, A47, Th37;
hence  contradiction by A46, VECTSP_4:11; ::_thesis: verum
end;
hence  ( L1 is not eigenvalue of fI & L2 is eigenvalue of fI ) by A4, A5, A43, A44, A45, Def2; ::_thesis: UnionKers (f + ((- L2) * (id V1))) is Subspace of I
 the carrier of (UnionKers (f + ((- L2) * (id V1)))) c= the carrier of I
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (UnionKers (f + ((- L2) * (id V1)))) or x in the carrier of I )
assume  x in the carrier of (UnionKers (f + ((- L2) * (id V1)))) ; ::_thesis: x in the carrier of I
then A48: x in UnionKers (f + ((- L2) * (id V1))) by STRUCT_0:def_5;
then  x in V1 by VECTSP_4:9;
then reconsider v = x as Vector of V1 by STRUCT_0:def_5;
 v is Vector of I by A7, A48;
hence  x in the carrier of I ; ::_thesis: verum
end;
hence  UnionKers (f + ((- L2) * (id V1))) is Subspace of I by VECTSP_4:27; ::_thesis: verum
end;

theorem :: VECTSP11:40
for K being Field
for V1 being VectSp of K
for U being finite Subset of V1 st U is linearly-independent holds
for u being Vector of V1 st u in U holds
for L being Linear_Combination of U \ {u} holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
proof
let K be Field; ::_thesis: for V1 being VectSp of K
for U being finite Subset of V1 st U is linearly-independent holds
for u being Vector of V1 st u in U holds
for L being Linear_Combination of U \ {u} holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
let V1 be VectSp of K; ::_thesis: for U being finite Subset of V1 st U is linearly-independent holds
for u being Vector of V1 st u in U holds
for L being Linear_Combination of U \ {u} holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
set V = V1;
let U be finite Subset of V1; ::_thesis: ( U is linearly-independent implies for u being Vector of V1 st u in U holds
for L being Linear_Combination of U \ {u} holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent ) )
assume A1: U is linearly-independent ; ::_thesis: for u being Vector of V1 st u in U holds
for L being Linear_Combination of U \ {u} holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
let u be Vector of V1; ::_thesis: ( u in U implies for L being Linear_Combination of U \ {u} holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent ) )
assume A2: u in U ; ::_thesis: for L being Linear_Combination of U \ {u} holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
defpred S1[ Nat] means  for L being Linear_Combination of U \ {u} st card (Carrier L) = $1 holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent );
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
 card U <> 0 by A2;
then reconsider C = (card U) - 1 as Element of NAT by NAT_1:20;
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; ::_thesis: S1[n + 1]
set n1 = n + 1;
let L be Linear_Combination of U \ {u}; ::_thesis: ( card (Carrier L) = n + 1 implies ( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent ) )
assume A5: card (Carrier L) = n + 1 ; ::_thesis: ( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
consider x being set  such that
A6: x in Carrier L by A5, CARD_1:27, XBOOLE_0:def_1;
A7: Carrier L c= U \ {u} by VECTSP_6:def_4;
then  x in U by A6, XBOOLE_0:def_5;
then A8: x <> 0. V1 by A1, VECTSP_7:2;
reconsider x = x as Vector of V1 by A6;
 x in {x} by TARSKI:def_1;
then  x in Lin {x} by VECTSP_7:8;
then consider X being Linear_Combination of {x} such that
A9: x = Sum X by VECTSP_7:7;
set Lx = L . x;
set LxX = (L . x) * X;
 ( Carrier ((L . x) * X) c= Carrier X & Carrier X c= {x} ) by VECTSP_6:28, VECTSP_6:def_4;
then A10: Carrier ((L . x) * X) c= {x} by XBOOLE_1:1;
then  ( Carrier (L - ((L . x) * X)) c= (Carrier L) \/ (Carrier ((L . x) * X)) & (Carrier L) \/ (Carrier ((L . x) * X)) c= (Carrier L) \/ {x} ) by VECTSP_6:41, XBOOLE_1:9;
then  Carrier (L - ((L . x) * X)) c= (Carrier L) \/ {x} by XBOOLE_1:1;
then A11: Carrier (L - ((L . x) * X)) c= Carrier L by A6, ZFMISC_1:40;
then  Carrier (L - ((L . x) * X)) c= U \ {u} by A7, XBOOLE_1:1;
then reconsider LLxX = L - ((L . x) * X) as Linear_Combination of U \ {u} by VECTSP_6:def_4;
A12: x in (U \ {u}) \/ {(u + (Sum LLxX))} by A6, A7, XBOOLE_0:def_3;
A13: (Carrier L) \ {x} c= Carrier (L - ((L . x) * X))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (Carrier L) \ {x} or y in Carrier (L - ((L . x) * X)) )
assume A14: y in (Carrier L) \ {x} ; ::_thesis: y in Carrier (L - ((L . x) * X))
 y in Carrier L by A14, XBOOLE_0:def_5;
then consider Y being Vector of V1 such that
A15: y = Y and
A16: L . Y <> 0. K ;
 not Y in Carrier ((L . x) * X) by A10, A14, A15, XBOOLE_0:def_5;
then  ((L . x) * X) . Y = 0. K ;
then (L - ((L . x) * X)) . Y = (L . Y) - (0. K) by VECTSP_6:40
.= L . Y by RLVECT_1:13 ;
hence  y in Carrier (L - ((L . x) * X)) by A15, A16; ::_thesis: verum
end;
(X . x) * x = x by A9, VECTSP_6:17
.= (1_ K) * x by VECTSP_1:def_17 ;
then A17: X . x = 1_ K by A8, VECTSP10:4;
(L - ((L . x) * X)) . x = (L . x) - (((L . x) * X) . x) by VECTSP_6:40
.= (L . x) - ((L . x) * (1_ K)) by A17, VECTSP_6:def_9
.= (L . x) - (L . x) by VECTSP_1:def_4
.= 0. K by RLVECT_1:5 ;
then  not x in Carrier (L - ((L . x) * X)) by VECTSP_6:2;
then  Carrier (L - ((L . x) * X)) c= (Carrier L) \ {x} by A11, ZFMISC_1:34;
then A18: Carrier (L - ((L . x) * X)) = (Carrier L) \ {x} by A13, XBOOLE_0:def_10;
 {x} c= Carrier L by A6, ZFMISC_1:31;
then  card (Carrier (L - ((L . x) * X))) = (n + 1) - (card {x}) by A5, A18, CARD_2:44
.= (n + 1) - 1 by CARD_1:30
.= n ;
then A19: (U \ {u}) \/ {(u + (Sum LLxX))} is linearly-independent by A4;
 u + (Sum LLxX) in {(u + (Sum LLxX))} by TARSKI:def_1;
then A20: u + (Sum LLxX) in (U \ {u}) \/ {(u + (Sum LLxX))} by XBOOLE_0:def_3;
A21: not u + (Sum L) in U \ {u}
proof
assume  u + (Sum L) in U \ {u} ; ::_thesis: contradiction
then A22: u + (Sum L) in Lin (U \ {u}) by VECTSP_7:8;
A23: (u + (Sum L)) - (Sum L) = u + ((Sum L) - (Sum L)) by RLVECT_1:def_3
.= u + (0. V1) by RLVECT_1:5
.= u by RLVECT_1:def_4 ;
 Sum L in Lin (U \ {u}) by VECTSP_7:7;
hence  contradiction by A1, A2, A22, A23, VECTSP_4:23, VECTSP_9:14; ::_thesis: verum
end;
 card U = C + 1 ;
then  card (U \ {u}) = C by A2, STIRL2_1:55;
then A24: card ((U \ {u}) \/ {(u + (Sum L))}) = C + 1 by A21, CARD_2:41;
Sum L = (0. V1) + (Sum L) by RLVECT_1:def_4
.= ((Sum ((L . x) * X)) + (- (Sum ((L . x) * X)))) + (Sum L) by RLVECT_1:5
.= (Sum ((L . x) * X)) + ((Sum L) - (Sum ((L . x) * X))) by RLVECT_1:def_3
.= (Sum ((L . x) * X)) + (Sum LLxX) by VECTSP_6:47
.= ((L . x) * x) + (Sum LLxX) by A9, VECTSP_6:45 ;
then A25: (u + (Sum LLxX)) + ((L . x) * x) = u + (Sum L) by RLVECT_1:def_3;
A26: not u + (Sum LLxX) in U \ {u}
proof
assume  u + (Sum LLxX) in U \ {u} ; ::_thesis: contradiction
then A27: u + (Sum LLxX) in Lin (U \ {u}) by VECTSP_7:8;
A28: (u + (Sum LLxX)) - (Sum LLxX) = u + ((Sum LLxX) - (Sum LLxX)) by RLVECT_1:def_3
.= u + (0. V1) by RLVECT_1:5
.= u by RLVECT_1:def_4 ;
 Sum LLxX in Lin (U \ {u}) by VECTSP_7:7;
hence  contradiction by A1, A2, A27, A28, VECTSP_4:23, VECTSP_9:14; ::_thesis: verum
end;
then A29: ((U \ {u}) \/ {(u + (Sum LLxX))}) \ {(u + (Sum LLxX))} = U \ {u} by ZFMISC_1:117;
 u + (Sum LLxX) <> x by A6, A7, A26;
hence  ( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent ) by A19, A25, A29, A20, A12, A24, MATRIX13:115; ::_thesis: verum
end;
let L be Linear_Combination of U \ {u}; ::_thesis: ( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
A30: S1[ 0 ]
proof
let L be Linear_Combination of U \ {u}; ::_thesis: ( card (Carrier L) = 0 implies ( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent ) )
assume  card (Carrier L) = 0 ; ::_thesis: ( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
then  Carrier L = {} ;
then u + (Sum L) = u + (0. V1) by VECTSP_6:19
.= u by RLVECT_1:def_4 ;
hence  ( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent ) by A1, A2, ZFMISC_1:116; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A30, A3);
then  S1[ card (Carrier L)] ;
hence  ( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent ) ; ::_thesis: verum
end;

theorem Th41: :: VECTSP11:41
for K being Field
for V1, V2 being VectSp of K
for A being Subset of V1
for L being Linear_Combination of V2
for f being linear-transformation of V1,V2 st Carrier L c= f .: A holds
ex M being Linear_Combination of A st f . (Sum M) = Sum L
proof
let K be Field; ::_thesis: for V1, V2 being VectSp of K
for A being Subset of V1
for L being Linear_Combination of V2
for f being linear-transformation of V1,V2 st Carrier L c= f .: A holds
ex M being Linear_Combination of A st f . (Sum M) = Sum L
let V1, V2 be VectSp of K; ::_thesis: for A being Subset of V1
for L being Linear_Combination of V2
for f being linear-transformation of V1,V2 st Carrier L c= f .: A holds
ex M being Linear_Combination of A st f . (Sum M) = Sum L
let A be Subset of V1; ::_thesis: for L being Linear_Combination of V2
for f being linear-transformation of V1,V2 st Carrier L c= f .: A holds
ex M being Linear_Combination of A st f . (Sum M) = Sum L
let L be Linear_Combination of V2; ::_thesis: for f being linear-transformation of V1,V2 st Carrier L c= f .: A holds
ex M being Linear_Combination of A st f . (Sum M) = Sum L
let f be linear-transformation of V1,V2; ::_thesis: ( Carrier L c= f .: A implies ex M being Linear_Combination of A st f . (Sum M) = Sum L )
assume A1: Carrier L c= f .: A ; ::_thesis: ex M being Linear_Combination of A st f . (Sum M) = Sum L
set C = Carrier L;
consider F being FinSequence of the carrier of V2 such that
A2: F is one-to-one and
A3: rng F = Carrier L and
A4: Sum L = Sum (L (#) F) by VECTSP_6:def_6;
defpred S1[ set , set ] means ( $2 in A & f . $2 = F . $1 );
set D = dom F;
A5: for x being set st x in dom F holds
ex y being set st
( y in the carrier of V1 & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in dom F implies ex y being set st
( y in the carrier of V1 & S1[x,y] ) )
assume  x in dom F ; ::_thesis: ex y being set st
( y in the carrier of V1 & S1[x,y] )
then  F . x in rng F by FUNCT_1:def_3;
then consider y being set  such that
 y in dom f and
A6: ( y in A & f . y = F . x ) by A1, A3, FUNCT_1:def_6;
take  y ; ::_thesis: ( y in the carrier of V1 & S1[x,y] )
thus  ( y in the carrier of V1 & S1[x,y] ) by A6; ::_thesis: verum
end;
consider p being Function of (dom F), the carrier of V1 such that
A7: for x being set st x in dom F holds
S1[x,p . x] from FUNCT_2:sch_1(A5);
A8: rng p c= the carrier of V1 by RELAT_1:def_19;
A9: dom p = dom F by FUNCT_2:def_1;
 dom F = Seg (len F) by FINSEQ_1:def_3;
then reconsider p = p as FinSequence by A9, FINSEQ_1:def_2;
reconsider p = p as FinSequence of V1 by A8, FINSEQ_1:def_4;
A10: now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_p_&_x2_in_dom_p_&_p_._x1_=_p_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom p & x2 in dom p & p . x1 = p . x2 implies x1 = x2 )
assume that
A11: ( x1 in dom p & x2 in dom p ) and
A12: p . x1 = p . x2 ; ::_thesis: x1 = x2
 ( f . (p . x1) = F . x1 & f . (p . x2) = F . x2 ) by A7, A9, A11;
hence  x1 = x2 by A2, A9, A11, A12, FUNCT_1:def_4; ::_thesis: verum
end;
then A13: p is one-to-one by FUNCT_1:def_4;
reconsider RNG = rng p as finite Subset of V1 by RELAT_1:def_19;
defpred S2[ set , set ] means ( ( $1 in rng p implies for x being set st x in dom F & p . x = $1 holds
$2 = L . (F . x) ) & ( not $1 in rng p implies $2 = 0. K ) );
A14: for x being set st x in the carrier of V1 holds
ex y being set st
( y in the carrier of K & S2[x,y] )
proof
let x be set ; ::_thesis: ( x in the carrier of V1 implies ex y being set st
( y in the carrier of K & S2[x,y] ) )
assume  x in the carrier of V1 ; ::_thesis: ex y being set st
( y in the carrier of K & S2[x,y] )
then reconsider v1 = x as Vector of V1 ;
percases ( not v1 in rng p or v1 in rng p ) ;
supposeA15: not v1 in rng p ; ::_thesis: ex y being set st
( y in the carrier of K & S2[x,y] )
take  0. K ; ::_thesis: ( 0. K in the carrier of K & S2[x, 0. K] )
thus  ( 0. K in the carrier of K & S2[x, 0. K] ) by A15; ::_thesis: verum
end;
supposeA16: v1 in rng p ; ::_thesis: ex y being set st
( y in the carrier of K & S2[x,y] )
then consider y being set  such that
A17: ( y in dom p & p . y = v1 ) by FUNCT_1:def_3;
take  L . (F . y) ; ::_thesis: ( L . (F . y) in the carrier of K & S2[x,L . (F . y)] )
 L . (F /. y) in the carrier of K ;
hence  ( L . (F . y) in the carrier of K & S2[x,L . (F . y)] ) by A9, A10, A16, A17, PARTFUN1:def_6; ::_thesis: verum
end;
end;
end;
consider M being Function of V1,K such that
A18: for x being set st x in the carrier of V1 holds
S2[x,M . x] from FUNCT_2:sch_1(A14);
reconsider M = M as Element of Funcs ( the carrier of V1, the carrier of K) by FUNCT_2:8;
 for v1 being Element of V1 st not v1 in RNG holds
M . v1 = 0. K by A18;
then reconsider M = M as Linear_Combination of V1 by VECTSP_6:def_1;
A19: Carrier M = RNG
proof
thus  Carrier M c= RNG :: according to XBOOLE_0:def_10 ::_thesis: RNG c= Carrier M
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier M or x in RNG )
assume A20: x in Carrier M ; ::_thesis: x in RNG
reconsider v1 = x as Vector of V1 by A20;
 M . v1 <> 0. K by A20, VECTSP_6:2;
hence  x in RNG by A18; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in RNG or y in Carrier M )
assume A21: y in RNG ; ::_thesis: y in Carrier M
reconsider v1 = y as Vector of V1 by A21;
consider x being set  such that
A22: x in dom F and
A23: p . x = v1 by A9, A21, FUNCT_1:def_3;
 F . x in Carrier L by A3, A22, FUNCT_1:def_3;
then A24: L . (F . x) <> 0. K by VECTSP_6:2;
 M . v1 = L . (F . x) by A18, A21, A22, A23;
hence  y in Carrier M by A24; ::_thesis: verum
end;
 RNG c= A
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in RNG or y in A )
assume  y in RNG ; ::_thesis: y in A
then  ex x being set st
( x in dom F & p . x = y ) by A9, FUNCT_1:def_3;
hence  y in A by A7; ::_thesis: verum
end;
then reconsider M = M as Linear_Combination of A by A19, VECTSP_6:def_4;
 len (M (#) p) = len p by VECTSP_6:def_5;
then A25: dom (M (#) p) = dom F by A9, FINSEQ_3:29;
 len (L (#) F) = len F by VECTSP_6:def_5;
then A26: dom (L (#) F) = dom F by FINSEQ_3:29;
A27: now__::_thesis:_for_x_being_set_st_x_in_dom_F_holds_
(f_*_(M_(#)_p))_._x_=_(L_(#)_F)_._x
let x be set ; ::_thesis: ( x in dom F implies (f * (M (#) p)) . x = (L (#) F) . x )
assume A28: x in dom F ; ::_thesis: (f * (M (#) p)) . x = (L (#) F) . x
reconsider i = x as Element of NAT by A28;
A29: F . i = F /. i by A28, PARTFUN1:def_6;
 p . i in RNG by A9, A28, FUNCT_1:def_3;
then A30: M . (p . i) = L . (F . i) by A18, A28;
A31: ( p /. i = p . i & f . (p . i) = F . i ) by A7, A9, A28, PARTFUN1:def_6;
thus (f * (M (#) p)) . x = f . ((M (#) p) . i) by A25, A28, FUNCT_1:13
.= f . ((M . (p /. i)) * (p /. i)) by A25, A28, VECTSP_6:def_5
.= (L . (F /. i)) * (F /. i) by A31, A29, A30, MOD_2:def_2
.= (L (#) F) . x by A26, A28, VECTSP_6:def_5 ; ::_thesis: verum
end;
take  M ; ::_thesis: f . (Sum M) = Sum L
 ( dom f = [#] V1 & rng (M (#) p) c= [#] V1 ) by FUNCT_2:def_1, RELAT_1:def_19;
then  dom (f * (M (#) p)) = dom (M (#) p) by RELAT_1:27;
then  f * (M (#) p) = L (#) F by A26, A25, A27, FUNCT_1:2;
hence  Sum L = f . (Sum (M (#) p)) by A4, MATRLIN:16
.= f . (Sum M) by A13, A19, VECTSP_6:def_6 ;
::_thesis: verum
end;

theorem :: VECTSP11:42
for K being Field
for V1, V2 being VectSp of K
for f being linear-transformation of V1,V2
for A being Subset of V1
for B being Subset of V2 st f .: A = B holds
f .: the carrier of (Lin A) = the carrier of (Lin B)
proof
let K be Field; ::_thesis: for V1, V2 being VectSp of K
for f being linear-transformation of V1,V2
for A being Subset of V1
for B being Subset of V2 st f .: A = B holds
f .: the carrier of (Lin A) = the carrier of (Lin B)
let V1, V2 be VectSp of K; ::_thesis: for f being linear-transformation of V1,V2
for A being Subset of V1
for B being Subset of V2 st f .: A = B holds
f .: the carrier of (Lin A) = the carrier of (Lin B)
let f be linear-transformation of V1,V2; ::_thesis: for A being Subset of V1
for B being Subset of V2 st f .: A = B holds
f .: the carrier of (Lin A) = the carrier of (Lin B)
A1: dom f = [#] V1 by FUNCT_2:def_1;
let A be Subset of V1; ::_thesis: for B being Subset of V2 st f .: A = B holds
f .: the carrier of (Lin A) = the carrier of (Lin B)
let B be Subset of V2; ::_thesis: ( f .: A = B implies f .: the carrier of (Lin A) = the carrier of (Lin B) )
assume A2: f .: A = B ; ::_thesis: f .: the carrier of (Lin A) = the carrier of (Lin B)
thus  f .: the carrier of (Lin A) c= the carrier of (Lin B) :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (Lin B) c= f .: the carrier of (Lin A)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: the carrier of (Lin A) or y in the carrier of (Lin B) )
assume  y in f .: the carrier of (Lin A) ; ::_thesis: y in the carrier of (Lin B)
then consider x being set  such that
 x in dom f and
A3: x in the carrier of (Lin A) and
A4: f . x = y by FUNCT_1:def_6;
 x in Lin A by A3, STRUCT_0:def_5;
then consider L being Linear_Combination of A such that
A5: x = Sum L by VECTSP_7:7;
consider F being FinSequence of V1 such that
 F is one-to-one and
A6: rng F = Carrier L and
A7: x = Sum (L (#) F) by A5, VECTSP_6:def_6;
set LF = L (#) F;
consider g being Function of NAT, the carrier of V1 such that
A8: x = g . (len (L (#) F)) and
A9: g . 0 = 0. V1 and
A10: for j being Element of NAT
for v being Vector of V1 st j < len (L (#) F) & v = (L (#) F) . (j + 1) holds
g . (j + 1) = (g . j) + v by A7, RLVECT_1:def_12;
defpred S1[ Nat] means ( $1 <= len F implies f . (g . $1) in Lin B );
A11: len (L (#) F) = len F by VECTSP_6:def_5;
then A12: dom (L (#) F) = dom F by FINSEQ_3:29;
A13: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A14: S1[n] ; ::_thesis: S1[n + 1]
reconsider N = n as Element of NAT by ORDINAL1:def_12;
reconsider gn = g . N as Vector of V1 ;
set N1 = N + 1;
assume A15: n + 1 <= len F ; ::_thesis: f . (g . (n + 1)) in Lin B
then A16: N < len F by NAT_1:13;
A17: ( Carrier L c= A & dom f = [#] V1 ) by FUNCT_2:def_1, VECTSP_6:def_4;
 1 <= n + 1 by NAT_1:14;
then A18: n + 1 in dom F by A15, FINSEQ_3:25;
then  ( F /. (N + 1) = F . (N + 1) & F . (N + 1) in Carrier L ) by A6, FUNCT_1:def_3, PARTFUN1:def_6;
then  f . (F /. (N + 1)) in B by A2, A17, FUNCT_1:def_6;
then A19: (L . (F /. (N + 1))) * (f . (F /. (N + 1))) in Lin B by VECTSP_4:21, VECTSP_7:8;
 (L (#) F) . (N + 1) = (L . (F /. (N + 1))) * (F /. (N + 1)) by A12, A18, VECTSP_6:def_5;
then  g . (N + 1) = gn + ((L . (F /. (N + 1))) * (F /. (N + 1))) by A11, A10, A16;
then f . (g . (n + 1)) = (f . gn) + (f . ((L . (F /. (N + 1))) * (F /. (N + 1)))) by VECTSP_1:def_20
.= (f . gn) + ((L . (F /. (N + 1))) * (f . (F /. (N + 1)))) by MOD_2:def_2 ;
hence  f . (g . (n + 1)) in Lin B by A14, A15, A19, NAT_1:13, VECTSP_4:20; ::_thesis: verum
end;
 f . (0. V1) = 0. V2 by RANKNULL:9;
then A20: S1[ 0 ] by A9, VECTSP_4:17;
 for n being Nat holds S1[n] from NAT_1:sch_2(A20, A13);
then  S1[ len F] ;
hence  y in the carrier of (Lin B) by A4, A11, A8, STRUCT_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (Lin B) or x in f .: the carrier of (Lin A) )
assume  x in the carrier of (Lin B) ; ::_thesis: x in f .: the carrier of (Lin A)
then  x in Lin B by STRUCT_0:def_5;
then consider L being Linear_Combination of B such that
A21: x = Sum L by VECTSP_7:7;
 Carrier L c= B by VECTSP_6:def_4;
then consider M being Linear_Combination of A such that
A22: f . (Sum M) = Sum L by A2, Th41;
 Sum M in Lin A by VECTSP_7:7;
then  Sum M in the carrier of (Lin A) by STRUCT_0:def_5;
hence  x in f .: the carrier of (Lin A) by A21, A22, A1, FUNCT_1:def_6; ::_thesis: verum
end;

theorem Th43: :: VECTSP11:43
for K being Field
for V1, V2 being VectSp of K
for L being Linear_Combination of V1
for F being FinSequence of V1
for f being linear-transformation of V1,V2 st f | ((Carrier L) /\ (rng F)) is one-to-one & rng F c= Carrier L holds
ex Lf being Linear_Combination of V2 st
( Carrier Lf = f .: ((Carrier L) /\ (rng F)) & f * (L (#) F) = Lf (#) (f * F) & ( for v1 being Vector of V1 st v1 in (Carrier L) /\ (rng F) holds
L . v1 = Lf . (f . v1) ) )
proof
let K be Field; ::_thesis: for V1, V2 being VectSp of K
for L being Linear_Combination of V1
for F being FinSequence of V1
for f being linear-transformation of V1,V2 st f | ((Carrier L) /\ (rng F)) is one-to-one & rng F c= Carrier L holds
ex Lf being Linear_Combination of V2 st
( Carrier Lf = f .: ((Carrier L) /\ (rng F)) & f * (L (#) F) = Lf (#) (f * F) & ( for v1 being Vector of V1 st v1 in (Carrier L) /\ (rng F) holds
L . v1 = Lf . (f . v1) ) )
let V1, V2 be VectSp of K; ::_thesis: for L being Linear_Combination of V1
for F being FinSequence of V1
for f being linear-transformation of V1,V2 st f | ((Carrier L) /\ (rng F)) is one-to-one & rng F c= Carrier L holds
ex Lf being Linear_Combination of V2 st
( Carrier Lf = f .: ((Carrier L) /\ (rng F)) & f * (L (#) F) = Lf (#) (f * F) & ( for v1 being Vector of V1 st v1 in (Carrier L) /\ (rng F) holds
L . v1 = Lf . (f . v1) ) )
let L be Linear_Combination of V1; ::_thesis: for F being FinSequence of V1
for f being linear-transformation of V1,V2 st f | ((Carrier L) /\ (rng F)) is one-to-one & rng F c= Carrier L holds
ex Lf being Linear_Combination of V2 st
( Carrier Lf = f .: ((Carrier L) /\ (rng F)) & f * (L (#) F) = Lf (#) (f * F) & ( for v1 being Vector of V1 st v1 in (Carrier L) /\ (rng F) holds
L . v1 = Lf . (f . v1) ) )
let F be FinSequence of V1; ::_thesis: for f being linear-transformation of V1,V2 st f | ((Carrier L) /\ (rng F)) is one-to-one & rng F c= Carrier L holds
ex Lf being Linear_Combination of V2 st
( Carrier Lf = f .: ((Carrier L) /\ (rng F)) & f * (L (#) F) = Lf (#) (f * F) & ( for v1 being Vector of V1 st v1 in (Carrier L) /\ (rng F) holds
L . v1 = Lf . (f . v1) ) )
let f be linear-transformation of V1,V2; ::_thesis: ( f | ((Carrier L) /\ (rng F)) is one-to-one & rng F c= Carrier L implies ex Lf being Linear_Combination of V2 st
( Carrier Lf = f .: ((Carrier L) /\ (rng F)) & f * (L (#) F) = Lf (#) (f * F) & ( for v1 being Vector of V1 st v1 in (Carrier L) /\ (rng F) holds
L . v1 = Lf . (f . v1) ) ) )
assume that
A1: f | ((Carrier L) /\ (rng F)) is one-to-one and
A2: rng F c= Carrier L ; ::_thesis: ex Lf being Linear_Combination of V2 st
( Carrier Lf = f .: ((Carrier L) /\ (rng F)) & f * (L (#) F) = Lf (#) (f * F) & ( for v1 being Vector of V1 st v1 in (Carrier L) /\ (rng F) holds
L . v1 = Lf . (f . v1) ) )
set R = rng F;
set C = Carrier L;
defpred S1[ set , set ] means ( ( not $1 in f .: ((Carrier L) /\ (rng F)) implies $2 = 0. K ) & ( $1 in f .: ((Carrier L) /\ (rng F)) implies for v1 being Vector of V1 st v1 in (Carrier L) /\ (rng F) & f . v1 = $1 holds
$2 = L . v1 ) );
A3: for x being set st x in the carrier of V2 holds
ex y being set st
( y in the carrier of K & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in the carrier of V2 implies ex y being set st
( y in the carrier of K & S1[x,y] ) )
assume  x in the carrier of V2 ; ::_thesis: ex y being set st
( y in the carrier of K & S1[x,y] )
percases ( not x in f .: ((Carrier L) /\ (rng F)) or x in f .: ((Carrier L) /\ (rng F)) ) ;
supposeA4: not x in f .: ((Carrier L) /\ (rng F)) ; ::_thesis: ex y being set st
( y in the carrier of K & S1[x,y] )
take  0. K ; ::_thesis: ( 0. K in the carrier of K & S1[x, 0. K] )
thus  ( 0. K in the carrier of K & S1[x, 0. K] ) by A4; ::_thesis: verum
end;
supposeA5: x in f .: ((Carrier L) /\ (rng F)) ; ::_thesis: ex y being set st
( y in the carrier of K & S1[x,y] )
then consider y being set  such that
 y in dom f and
A6: y in (Carrier L) /\ (rng F) and
A7: x = f . y by FUNCT_1:def_6;
reconsider y = y as Vector of V1 by A6;
take  L . y ; ::_thesis: ( L . y in the carrier of K & S1[x,L . y] )
now__::_thesis:_for_v1_being_Vector_of_V1_st_v1_in_(Carrier_L)_/\_(rng_F)_&_f_._v1_=_x_holds_
L_._y_=_L_._v1
A8: dom f = [#] V1 by FUNCT_2:def_1;
then A9: y in dom (f | ((Carrier L) /\ (rng F))) by A6, RELAT_1:57;
A10: (f | ((Carrier L) /\ (rng F))) . y = x by A6, A7, FUNCT_1:49;
let v1 be Vector of V1; ::_thesis: ( v1 in (Carrier L) /\ (rng F) & f . v1 = x implies L . y = L . v1 )
assume that
A11: v1 in (Carrier L) /\ (rng F) and
A12: f . v1 = x ; ::_thesis: L . y = L . v1
A13: (f | ((Carrier L) /\ (rng F))) . v1 = x by A11, A12, FUNCT_1:49;
 v1 in dom (f | ((Carrier L) /\ (rng F))) by A11, A8, RELAT_1:57;
hence  L . y = L . v1 by A1, A9, A13, A10, FUNCT_1:def_4; ::_thesis: verum
end;
hence  ( L . y in the carrier of K & S1[x,L . y] ) by A5; ::_thesis: verum
end;
end;
end;
consider Lf being Function of V2,K such that
A14: for x being set st x in the carrier of V2 holds
S1[x,Lf . x] from FUNCT_2:sch_1(A3);
reconsider Lf = Lf as Element of Funcs ( the carrier of V2, the carrier of K) by FUNCT_2:8;
 for v2 being Element of V2 st not v2 in f .: ((Carrier L) /\ (rng F)) holds
Lf . v2 = 0. K by A14;
then reconsider Lf = Lf as Linear_Combination of V2 by VECTSP_6:def_1;
A15: dom f = [#] V1 by FUNCT_2:def_1;
take  Lf ; ::_thesis: ( Carrier Lf = f .: ((Carrier L) /\ (rng F)) & f * (L (#) F) = Lf (#) (f * F) & ( for v1 being Vector of V1 st v1 in (Carrier L) /\ (rng F) holds
L . v1 = Lf . (f . v1) ) )
A16: f .: ((Carrier L) /\ (rng F)) c= Carrier Lf
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: ((Carrier L) /\ (rng F)) or y in Carrier Lf )
assume A17: y in f .: ((Carrier L) /\ (rng F)) ; ::_thesis: y in Carrier Lf
consider v1 being set  such that
 v1 in dom f and
A18: v1 in (Carrier L) /\ (rng F) and
A19: f . v1 = y by A17, FUNCT_1:def_6;
reconsider v1 = v1 as Vector of V1 by A18;
 v1 in Carrier L by A18, XBOOLE_0:def_4;
then A20: L . v1 <> 0. K by VECTSP_6:2;
reconsider v2 = y as Vector of V2 by A17;
 Lf . v2 = L . v1 by A14, A17, A18, A19;
hence  y in Carrier Lf by A20; ::_thesis: verum
end;
 Carrier Lf c= f .: ((Carrier L) /\ (rng F))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier Lf or x in f .: ((Carrier L) /\ (rng F)) )
assume A21: x in Carrier Lf ; ::_thesis: x in f .: ((Carrier L) /\ (rng F))
reconsider v2 = x as Vector of V2 by A21;
 Lf . v2 <> 0. K by A21, VECTSP_6:2;
hence  x in f .: ((Carrier L) /\ (rng F)) by A14; ::_thesis: verum
end;
hence  Carrier Lf = f .: ((Carrier L) /\ (rng F)) by A16, XBOOLE_0:def_10; ::_thesis: ( f * (L (#) F) = Lf (#) (f * F) & ( for v1 being Vector of V1 st v1 in (Carrier L) /\ (rng F) holds
L . v1 = Lf . (f . v1) ) )
 len (L (#) F) = len F by VECTSP_6:def_5;
then A22: dom (L (#) F) = dom F by FINSEQ_3:29;
 rng F c= [#] V1 by RELAT_1:def_19;
then A23: dom (f * F) = dom F by A15, RELAT_1:27;
 len (Lf (#) (f * F)) = len (f * F) by VECTSP_6:def_5;
then A24: dom (Lf (#) (f * F)) = dom (f * F) by FINSEQ_3:29;
A25: now__::_thesis:_for_x_being_set_st_x_in_dom_F_holds_
(f_*_(L_(#)_F))_._x_=_(Lf_(#)_(f_*_F))_._x
let x be set ; ::_thesis: ( x in dom F implies (f * (L (#) F)) . x = (Lf (#) (f * F)) . x )
assume A26: x in dom F ; ::_thesis: (f * (L (#) F)) . x = (Lf (#) (f * F)) . x
reconsider k = x as Nat by A26;
A27: (f * F) . k = (f * F) /. k by A23, A26, PARTFUN1:def_6;
A28: F /. k = F . k by A26, PARTFUN1:def_6;
then A29: (f * F) . k = f . (F /. k) by A23, A26, FUNCT_1:12;
 F . k in rng F by A26, FUNCT_1:def_3;
then A30: F . k in (Carrier L) /\ (rng F) by A2, XBOOLE_0:def_4;
then  (f * F) /. k in f .: ((Carrier L) /\ (rng F)) by A15, A28, A29, A27, FUNCT_1:def_6;
then A31: L . (F /. k) = Lf . ((f * F) /. k) by A14, A28, A29, A27, A30;
thus (f * (L (#) F)) . x = f . ((L (#) F) . k) by A22, A26, FUNCT_1:13
.= f . ((L . (F /. k)) * (F /. k)) by A22, A26, VECTSP_6:def_5
.= (Lf . ((f * F) /. k)) * ((f * F) /. k) by A29, A27, A31, MOD_2:def_2
.= (Lf (#) (f * F)) . x by A24, A23, A26, VECTSP_6:def_5 ; ::_thesis: verum
end;
 rng (L (#) F) c= [#] V1 by RELAT_1:def_19;
then  dom (f * (L (#) F)) = dom (L (#) F) by A15, RELAT_1:27;
hence  f * (L (#) F) = Lf (#) (f * F) by A22, A24, A23, A25, FUNCT_1:2; ::_thesis: for v1 being Vector of V1 st v1 in (Carrier L) /\ (rng F) holds
L . v1 = Lf . (f . v1)
let v1 be Vector of V1; ::_thesis: ( v1 in (Carrier L) /\ (rng F) implies L . v1 = Lf . (f . v1) )
assume A32: v1 in (Carrier L) /\ (rng F) ; ::_thesis: L . v1 = Lf . (f . v1)
 f . v1 in f .: ((Carrier L) /\ (rng F)) by A15, A32, FUNCT_1:def_6;
hence  L . v1 = Lf . (f . v1) by A14, A32; ::_thesis: verum
end;

theorem :: VECTSP11:44
for K being Field
for V1, V2 being VectSp of K
for A, B being Subset of V1
for L being Linear_Combination of V1 st Carrier L c= A \/ B & Sum L = 0. V1 holds
for f being additive homogeneous Function of V1,V2 st f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} holds
Carrier L c= A
proof
let K be Field; ::_thesis: for V1, V2 being VectSp of K
for A, B being Subset of V1
for L being Linear_Combination of V1 st Carrier L c= A \/ B & Sum L = 0. V1 holds
for f being additive homogeneous Function of V1,V2 st f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} holds
Carrier L c= A
let V1, V2 be VectSp of K; ::_thesis: for A, B being Subset of V1
for L being Linear_Combination of V1 st Carrier L c= A \/ B & Sum L = 0. V1 holds
for f being additive homogeneous Function of V1,V2 st f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} holds
Carrier L c= A
let A, B be Subset of V1; ::_thesis: for L being Linear_Combination of V1 st Carrier L c= A \/ B & Sum L = 0. V1 holds
for f being additive homogeneous Function of V1,V2 st f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} holds
Carrier L c= A
let L be Linear_Combination of V1; ::_thesis: ( Carrier L c= A \/ B & Sum L = 0. V1 implies for f being additive homogeneous Function of V1,V2 st f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} holds
Carrier L c= A )
assume that
A1: Carrier L c= A \/ B and
A2: Sum L = 0. V1 ; ::_thesis: for f being additive homogeneous Function of V1,V2 st f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} holds
Carrier L c= A
consider F being FinSequence of V1 such that
A3: F is one-to-one and
A4: rng F = Carrier L and
A5: 0. V1 = Sum (L (#) F) by A2, VECTSP_6:def_6;
let f be additive homogeneous Function of V1,V2; ::_thesis: ( f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} implies Carrier L c= A )
assume that
A6: f | B is one-to-one and
A7: f .: B is linearly-independent Subset of V2 and
A8: f .: A c= {(0. V2)} ; ::_thesis: Carrier L c= A
percases ( dom F = {} or dom F <> {} ) ;
suppose dom F = {} ; ::_thesis: Carrier L c= A
then  rng F = {} by RELAT_1:42;
hence  Carrier L c= A by A4, XBOOLE_1:2; ::_thesis: verum
end;
suppose dom F <> {} ; ::_thesis: Carrier L c= A
then reconsider D = dom F as non empty finite set ;
set C = Carrier L;
set FA = F " ((Carrier L) /\ A);
set FB = F " ((Carrier L) /\ B);
set SS = (Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A)));
A9: (Carrier L) /\ ((Carrier L) /\ B) = (Carrier L) /\ B by XBOOLE_1:18, XBOOLE_1:28;
 rng F c= the carrier of V1 by RELAT_1:def_19;
then reconsider F9 = F as Function of D, the carrier of V1 by FUNCT_2:2;
A10: D = Seg (len F) by FINSEQ_1:def_3;
then A11: Sgm (F " ((Carrier L) /\ A)) is one-to-one by FINSEQ_3:92, RELAT_1:132;
A12: ( len (Sgm (F " ((Carrier L) /\ A))) = card (F " ((Carrier L) /\ A)) & len (Sgm (F " ((Carrier L) /\ B))) = card (F " ((Carrier L) /\ B)) ) by A10, FINSEQ_3:39, RELAT_1:132;
A13: Sgm (F " ((Carrier L) /\ B)) is one-to-one by A10, FINSEQ_3:92, RELAT_1:132;
A14: F " ((Carrier L) /\ B) c= D by RELAT_1:132;
then A15: rng (Sgm (F " ((Carrier L) /\ B))) = F " ((Carrier L) /\ B) by A10, FINSEQ_1:def_13;
A16: F " ((Carrier L) /\ A) c= D by RELAT_1:132;
then A17: rng (Sgm (F " ((Carrier L) /\ A))) = F " ((Carrier L) /\ A) by A10, FINSEQ_1:def_13;
then reconsider SA = Sgm (F " ((Carrier L) /\ A)), SB = Sgm (F " ((Carrier L) /\ B)) as FinSequence of D by A16, A14, A15, FINSEQ_1:def_4;
 A misses B
proof
assume  A meets B ; ::_thesis: contradiction
then consider x being set  such that
A18: x in A and
A19: x in B by XBOOLE_0:3;
reconsider x = x as Vector of V1 by A18;
 dom f = the carrier of V1 by FUNCT_2:def_1;
then  ( f . x in f .: A & f . x in f .: B ) by A18, A19, FUNCT_1:def_6;
then  0. V2 in f .: B by A8, TARSKI:def_1;
hence  contradiction by A7, VECTSP_7:2; ::_thesis: verum
end;
then A20: (Carrier L) /\ A misses (Carrier L) /\ B by XBOOLE_1:76;
then  F " ((Carrier L) /\ A) misses F " ((Carrier L) /\ B) by FUNCT_1:71;
then A21: (Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A))) is one-to-one by A11, A17, A13, A15, FINSEQ_3:91;
((Carrier L) /\ A) \/ ((Carrier L) /\ B) = (Carrier L) /\ (A \/ B) by XBOOLE_1:23
.= Carrier L by A1, XBOOLE_1:28 ;
then A22: (F " ((Carrier L) /\ A)) \/ (F " ((Carrier L) /\ B)) = F " (Carrier L) by RELAT_1:140
.= dom F by A4, RELAT_1:134 ;
then (card (F " ((Carrier L) /\ A))) + (card (F " ((Carrier L) /\ B))) = card (Seg (len F)) by A10, A20, CARD_2:40, FUNCT_1:71
.= len F by FINSEQ_1:57 ;
then  len ((Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A)))) = len F by A12, FINSEQ_1:22;
then A23: dom ((Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A)))) = D by FINSEQ_3:29;
 rng ((Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A)))) = D by A22, A17, A15, FINSEQ_1:31;
then reconsider SS = (Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A))) as Function of D,D by A23, FUNCT_2:1;
 card D = card D ;
then  SS is onto by A21, STIRL2_1:60;
then reconsider SS = SS as Permutation of D by A21;
reconsider FS = F9 * SS, FSA = F9 * SA, FSB = F9 * SB as FinSequence of V1 by FINSEQ_2:47;
A24: (Carrier L) /\ B c= rng FSB
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (Carrier L) /\ B or y in rng FSB )
assume A25: y in (Carrier L) /\ B ; ::_thesis: y in rng FSB
 y in rng F by A4, A25, XBOOLE_0:def_4;
then consider x being set  such that
A26: ( x in dom F & y = F . x ) by FUNCT_1:def_3;
 x in F " ((Carrier L) /\ B) by A25, A26, FUNCT_1:def_7;
then consider z being set  such that
A27: ( z in dom SB & SB . z = x ) by A15, FUNCT_1:def_3;
 ( FSB . z = y & z in dom FSB ) by A26, A27, FUNCT_1:11, FUNCT_1:13;
hence  y in rng FSB by FUNCT_1:def_3; ::_thesis: verum
end;
 rng FSB c= (Carrier L) /\ B
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng FSB or y in (Carrier L) /\ B )
assume  y in rng FSB ; ::_thesis: y in (Carrier L) /\ B
then consider x being set  such that
A28: x in dom FSB and
A29: FSB . x = y by FUNCT_1:def_3;
 x in dom SB by A28, FUNCT_1:11;
then A30: SB . x in F " ((Carrier L) /\ B) by A15, FUNCT_1:def_3;
 FSB . x = F . (SB . x) by A28, FUNCT_1:12;
hence  y in (Carrier L) /\ B by A29, A30, FUNCT_1:def_7; ::_thesis: verum
end;
then A31: (Carrier L) /\ B = rng FSB by A24, XBOOLE_0:def_10;
A32: now__::_thesis:_for_k_being_Element_of_NAT_
for_v_being_Element_of_V2_st_k_in_dom_(f_*_(L_(#)_FSA))_&_v_=_(f_*_(L_(#)_FSA))_._k_holds_
(f_*_(L_(#)_FSA))_._k_=_(0._K)_*_v
 len (L (#) FSA) = len FSA by VECTSP_6:def_5;
then A33: dom (L (#) FSA) = dom FSA by FINSEQ_3:29;
A34: dom f = [#] V1 by FUNCT_2:def_1;
 ( rng (L (#) FSA) c= [#] V1 & dom f = [#] V1 ) by FUNCT_2:def_1, RELAT_1:def_19;
then A35: dom (f * (L (#) FSA)) = dom (L (#) FSA) by RELAT_1:27;
let k be Element of NAT ; ::_thesis: for v being Element of V2 st k in dom (f * (L (#) FSA)) & v = (f * (L (#) FSA)) . k holds
(f * (L (#) FSA)) . k = (0. K) * v
let v be Element of V2; ::_thesis: ( k in dom (f * (L (#) FSA)) & v = (f * (L (#) FSA)) . k implies (f * (L (#) FSA)) . k = (0. K) * v )
assume that
A36: k in dom (f * (L (#) FSA)) and
 v = (f * (L (#) FSA)) . k ; ::_thesis: (f * (L (#) FSA)) . k = (0. K) * v
 dom FSA = dom SA by A17, RELAT_1:27, RELAT_1:132;
then  SA . k in F " ((Carrier L) /\ A) by A17, A36, A35, A33, FUNCT_1:def_3;
then A37: F . (SA . k) in (Carrier L) /\ A by FUNCT_1:def_7;
FSA /. k = FSA . k by A36, A35, A33, PARTFUN1:def_6
.= F . (SA . k) by A36, A35, A33, FUNCT_1:12 ;
then  FSA /. k in A by A37, XBOOLE_0:def_4;
then  f . (FSA /. k) in f .: A by A34, FUNCT_1:def_6;
then A38: f . (FSA /. k) = 0. V2 by A8, TARSKI:def_1;
thus (f * (L (#) FSA)) . k = f . ((L (#) FSA) . k) by A36, FUNCT_1:12
.= f . ((L . (FSA /. k)) * (FSA /. k)) by A36, A35, VECTSP_6:def_5
.= (L . (FSA /. k)) * (0. V2) by A38, MOD_2:def_2
.= 0. V2 by VECTSP_1:14
.= (0. K) * v by VECTSP_1:14 ; ::_thesis: verum
end;
 len (f * (L (#) FSA)) = len (f * (L (#) FSA)) ;
then A39: Sum (f * (L (#) FSA)) = (0. K) * (Sum (f * (L (#) FSA))) by A32, RLVECT_2:66;
 FS = FSB ^ FSA by FINSEQOP:9;
then  L (#) FS = (L (#) FSB) ^ (L (#) FSA) by VECTSP_6:13;
then A40: f * (L (#) FS) = (f * (L (#) FSB)) ^ (f * (L (#) FSA)) by FINSEQOP:9;
 (f | B) | ((Carrier L) /\ B) = f | ((Carrier L) /\ B) by RELAT_1:74, XBOOLE_1:18;
then A41: f | ((Carrier L) /\ B) is one-to-one by A6, FUNCT_1:52;
then consider Lf being Linear_Combination of V2 such that
A42: Carrier Lf = f .: ((Carrier L) /\ (rng FSB)) and
A43: f * (L (#) FSB) = Lf (#) (f * FSB) and
A44: for v1 being Vector of V1 st v1 in (Carrier L) /\ (rng FSB) holds
L . v1 = Lf . (f . v1) by A31, A9, Th43, XBOOLE_1:18;
A45: Carrier Lf = rng (f * FSB) by A31, A9, A42, RELAT_1:127;
A46: f * FSB = f * ((id (rng FSB)) * FSB) by RELAT_1:53
.= (f * (id (rng FSB))) * FSB by RELAT_1:36
.= (f | ((Carrier L) /\ B)) * FSB by A31, RELAT_1:65 ;
 Carrier Lf c= f .: B by A31, A9, A42, RELAT_1:123, XBOOLE_1:18;
then A47: Lf is Linear_Combination of f .: B by VECTSP_6:def_4;
 f . (0. V1) = 0. V2 by RANKNULL:9;
then A48: 0. V2 = f . (Sum (L (#) FS)) by A5, VECTSP_9:1
.= Sum (f * (L (#) FS)) by MATRLIN:16
.= (Sum (f * (L (#) FSB))) + (Sum (f * (L (#) FSA))) by A40, RLVECT_1:41
.= (Sum (f * (L (#) FSB))) + (0. V2) by A39, VECTSP_1:14
.= Sum (Lf (#) (f * FSB)) by A43, RLVECT_1:def_4
.= Sum Lf by A3, A13, A41, A45, A46, VECTSP_6:def_6 ;
thus  Carrier L c= A ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier L or x in A )
assume A49: x in Carrier L ; ::_thesis: x in A
reconsider v1 = x as Vector of V1 by A49;
assume A50: not x in A ; ::_thesis: contradiction
 ( x in A or x in B ) by A1, A49, XBOOLE_0:def_3;
then  v1 in (Carrier L) /\ (rng FSB) by A31, A9, A49, A50, XBOOLE_0:def_4;
then A51: L . v1 = Lf . (f . v1) by A44;
 not f . v1 in Carrier Lf by A7, A47, A48, VECTSP_7:def_1;
then  L . v1 = 0. K by A51;
hence  contradiction by A49, VECTSP_6:2; ::_thesis: verum
end;
end;
end;
end;