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 S₁[ 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 S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[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_0:26;
defpred S₂[ 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_0:24;
A8: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A9: S₂[k] ; :: thesis: S₂[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;

per cases ( k = 0 or k >= 1 ) by NAT_1:14;

suppose A14: 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 ;
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 3
.= 1_ K ;
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 ;
1 <= n + 1 by A10, A11, XXREAL_0:2;
then 1 <= len (LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) by A23;
then 1 in dom (LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) by FINSEQ_3:25;
then (LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) . 1 = (LaplaceExpL ((A + (x * (1. (K,(n + 1))))),1)) /. 1 by PARTFUN1:def 6;
hence 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;

suppose A25: 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)))
.= ((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 3
.= ((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: S₂[ 0 ] ;
for k being Nat holds S₂[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: S₁[ 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 S₁[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