let n be Nat; :: thesis: for p1 being Element of Permutations (n + 1)

for K being Field

for i, j being Nat st i in Seg (n + 1) & p1 . i = j holds

for M being Matrix of n + 1,K

for DM being Matrix of n,K st DM = Delete (M,i,j) holds

(Path_product M) . p1 = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i)))

let p1 be Element of Permutations (n + 1); :: thesis: for K being Field

for i, j being Nat st i in Seg (n + 1) & p1 . i = j holds

for M being Matrix of n + 1,K

for DM being Matrix of n,K st DM = Delete (M,i,j) holds

(Path_product M) . p1 = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i)))

let K be Field; :: thesis: for i, j being Nat st i in Seg (n + 1) & p1 . i = j holds

for M being Matrix of n + 1,K

for DM being Matrix of n,K st DM = Delete (M,i,j) holds

(Path_product M) . p1 = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i)))

reconsider N = n as Element of NAT by ORDINAL1:def 12;

set n1 = N + 1;

let i, j be Nat; :: thesis: ( i in Seg (n + 1) & p1 . i = j implies for M being Matrix of n + 1,K

for DM being Matrix of n,K st DM = Delete (M,i,j) holds

(Path_product M) . p1 = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i))) )

assume that

A1: i in Seg (n + 1) and

A2: p1 . i = j ; :: thesis: for M being Matrix of n + 1,K

for DM being Matrix of n,K st DM = Delete (M,i,j) holds

(Path_product M) . p1 = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i)))

set mm = the multF of K;

set R = Rem (p1,i);

let M be Matrix of n + 1,K; :: thesis: for DM being Matrix of n,K st DM = Delete (M,i,j) holds

(Path_product M) . p1 = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i)))

let DM be Matrix of n,K; :: thesis: ( DM = Delete (M,i,j) implies (Path_product M) . p1 = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i))) )

assume A3: DM = Delete (M,i,j) ; :: thesis: (Path_product M) . p1 = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i)))

set PR = Path_matrix ((Rem (p1,i)),DM);

set Pp1 = Path_matrix (p1,M);

len (Path_matrix (p1,M)) = N + 1 by MATRIX_3:def 7;

then dom (Path_matrix (p1,M)) = Seg (N + 1) by FINSEQ_1:def 3;

then A4: (Path_matrix (p1,M)) . i = M * (i,j) by A1, A2, MATRIX_3:def 7;

for K being Field

for i, j being Nat st i in Seg (n + 1) & p1 . i = j holds

for M being Matrix of n + 1,K

for DM being Matrix of n,K st DM = Delete (M,i,j) holds

(Path_product M) . p1 = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i)))

let p1 be Element of Permutations (n + 1); :: thesis: for K being Field

for i, j being Nat st i in Seg (n + 1) & p1 . i = j holds

for M being Matrix of n + 1,K

for DM being Matrix of n,K st DM = Delete (M,i,j) holds

(Path_product M) . p1 = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i)))

let K be Field; :: thesis: for i, j being Nat st i in Seg (n + 1) & p1 . i = j holds

for M being Matrix of n + 1,K

for DM being Matrix of n,K st DM = Delete (M,i,j) holds

(Path_product M) . p1 = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i)))

reconsider N = n as Element of NAT by ORDINAL1:def 12;

set n1 = N + 1;

let i, j be Nat; :: thesis: ( i in Seg (n + 1) & p1 . i = j implies for M being Matrix of n + 1,K

for DM being Matrix of n,K st DM = Delete (M,i,j) holds

(Path_product M) . p1 = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i))) )

assume that

A1: i in Seg (n + 1) and

A2: p1 . i = j ; :: thesis: for M being Matrix of n + 1,K

for DM being Matrix of n,K st DM = Delete (M,i,j) holds

(Path_product M) . p1 = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i)))

set mm = the multF of K;

set R = Rem (p1,i);

let M be Matrix of n + 1,K; :: thesis: for DM being Matrix of n,K st DM = Delete (M,i,j) holds

(Path_product M) . p1 = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i)))

let DM be Matrix of n,K; :: thesis: ( DM = Delete (M,i,j) implies (Path_product M) . p1 = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i))) )

assume A3: DM = Delete (M,i,j) ; :: thesis: (Path_product M) . p1 = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i)))

set PR = Path_matrix ((Rem (p1,i)),DM);

set Pp1 = Path_matrix (p1,M);

len (Path_matrix (p1,M)) = N + 1 by MATRIX_3:def 7;

then dom (Path_matrix (p1,M)) = Seg (N + 1) by FINSEQ_1:def 3;

then A4: (Path_matrix (p1,M)) . i = M * (i,j) by A1, A2, MATRIX_3:def 7;

A5: now :: thesis: the multF of K $$ (Path_matrix (p1,M)) = (M * (i,j)) * ( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM)))end;

per cases
( N = 0 or N > 0 )
;

end;

suppose A6:
N = 0
; :: thesis: the multF of K $$ (Path_matrix (p1,M)) = (M * (i,j)) * ( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM)))

then A7:
len (Path_matrix (p1,M)) = 1
by MATRIX_3:def 7;

(Path_matrix (p1,M)) . 1 = M * (i,j) by A1, A4, A6, FINSEQ_1:2, TARSKI:def 1;

then Path_matrix (p1,M) = <*(M * (i,j))*> by A7, FINSEQ_1:40;

then A8: the multF of K $$ (Path_matrix (p1,M)) = M * (i,j) by FINSOP_1:11;

len (Path_matrix ((Rem (p1,i)),DM)) = 0 by A6, MATRIX_3:def 7;

then Path_matrix ((Rem (p1,i)),DM) = <*> the carrier of K ;

then A9: the multF of K $$ (Path_matrix ((Rem (p1,i)),DM)) = the_unity_wrt the multF of K by FINSOP_1:10;

the_unity_wrt the multF of K = 1_ K by FVSUM_1:5;

hence the multF of K $$ (Path_matrix (p1,M)) = (M * (i,j)) * ( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM))) by A8, A9; :: thesis: verum

end;(Path_matrix (p1,M)) . 1 = M * (i,j) by A1, A4, A6, FINSEQ_1:2, TARSKI:def 1;

then Path_matrix (p1,M) = <*(M * (i,j))*> by A7, FINSEQ_1:40;

then A8: the multF of K $$ (Path_matrix (p1,M)) = M * (i,j) by FINSOP_1:11;

len (Path_matrix ((Rem (p1,i)),DM)) = 0 by A6, MATRIX_3:def 7;

then Path_matrix ((Rem (p1,i)),DM) = <*> the carrier of K ;

then A9: the multF of K $$ (Path_matrix ((Rem (p1,i)),DM)) = the_unity_wrt the multF of K by FINSOP_1:10;

the_unity_wrt the multF of K = 1_ K by FVSUM_1:5;

hence the multF of K $$ (Path_matrix (p1,M)) = (M * (i,j)) * ( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM))) by A8, A9; :: thesis: verum

suppose A10:
N > 0
; :: thesis: the multF of K $$ (Path_matrix (p1,M)) = (M * (i,j)) * ( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM)))

len (Path_matrix ((Rem (p1,i)),DM)) = n
by MATRIX_3:def 7;

then consider f being sequence of the carrier of K such that

A11: f . 1 = (Path_matrix ((Rem (p1,i)),DM)) . 1 and

A12: for k being Nat st 0 <> k & k < n holds

f . (k + 1) = the multF of K . ((f . k),((Path_matrix ((Rem (p1,i)),DM)) . (k + 1))) and

A13: the multF of K $$ (Path_matrix ((Rem (p1,i)),DM)) = f . n by A10, FINSOP_1:def 1;

len (Path_matrix (p1,M)) = N + 1 by MATRIX_3:def 7;

then consider F being sequence of the carrier of K such that

A14: F . 1 = (Path_matrix (p1,M)) . 1 and

A15: for k being Nat st 0 <> k & k < N + 1 holds

F . (k + 1) = the multF of K . ((F . k),((Path_matrix (p1,M)) . (k + 1))) and

A16: the multF of K $$ (Path_matrix (p1,M)) = F . (N + 1) by FINSOP_1:def 1;

defpred S_{1}[ Nat] means ( 1 <= $1 & $1 < i implies f . $1 = F . $1 );

A17: for k being Nat st k in Seg n holds

( ( k < i implies (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . k ) & ( k >= i implies (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . (k + 1) ) )_{1}[k] holds

S_{1}[k + 1]
_{2}[ Nat] means ( i <= $1 & $1 <= N + 1 implies ( ( $1 = 1 implies F . $1 = M * (i,j) ) & ( $1 > 1 implies for a being Element of K st a = f . ($1 - 1) holds

F . $1 = (M * (i,j)) * a ) ) );

A41: S_{1}[ 0 ]
;

A42: for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A41, A32);

A43: for k being Nat st S_{2}[k] holds

S_{2}[k + 1]
_{2}[ 0 ]
;

A64: for k being Nat holds S_{2}[k]
from NAT_1:sch 2(A63, A43);

A65: i <= N + 1 by A1, FINSEQ_1:1;

A66: (N + 1) - 1 = n ;

N + 1 > 0 + 1 by A10, XREAL_1:6;

hence the multF of K $$ (Path_matrix (p1,M)) = (M * (i,j)) * ( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM))) by A16, A13, A64, A65, A66; :: thesis: verum

end;then consider f being sequence of the carrier of K such that

A11: f . 1 = (Path_matrix ((Rem (p1,i)),DM)) . 1 and

A12: for k being Nat st 0 <> k & k < n holds

f . (k + 1) = the multF of K . ((f . k),((Path_matrix ((Rem (p1,i)),DM)) . (k + 1))) and

A13: the multF of K $$ (Path_matrix ((Rem (p1,i)),DM)) = f . n by A10, FINSOP_1:def 1;

len (Path_matrix (p1,M)) = N + 1 by MATRIX_3:def 7;

then consider F being sequence of the carrier of K such that

A14: F . 1 = (Path_matrix (p1,M)) . 1 and

A15: for k being Nat st 0 <> k & k < N + 1 holds

F . (k + 1) = the multF of K . ((F . k),((Path_matrix (p1,M)) . (k + 1))) and

A16: the multF of K $$ (Path_matrix (p1,M)) = F . (N + 1) by FINSOP_1:def 1;

defpred S

A17: for k being Nat st k in Seg n holds

( ( k < i implies (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . k ) & ( k >= i implies (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . (k + 1) ) )

proof

A32:
for k being Nat st S
len (Path_matrix (p1,M)) = N + 1
by MATRIX_3:def 7;

then A18: dom (Path_matrix (p1,M)) = Seg (N + 1) by FINSEQ_1:def 3;

len (Path_matrix ((Rem (p1,i)),DM)) = n by MATRIX_3:def 7;

then A19: dom (Path_matrix ((Rem (p1,i)),DM)) = Seg n by FINSEQ_1:def 3;

reconsider p19 = p1 as Permutation of (Seg (N + 1)) by MATRIX_1:def 12;

reconsider R9 = Rem (p1,i) as Permutation of (Seg n) by MATRIX_1:def 12;

let k be Nat; :: thesis: ( k in Seg n implies ( ( k < i implies (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . k ) & ( k >= i implies (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . (k + 1) ) ) )

assume A20: k in Seg n ; :: thesis: ( ( k < i implies (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . k ) & ( k >= i implies (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . (k + 1) ) )

reconsider k1 = k + 1 as Element of NAT ;

A21: k1 in Seg (N + 1) by A20, FINSEQ_1:60;

A22: rng p19 = Seg (N + 1) by FUNCT_2:def 3;

dom p19 = Seg (N + 1) by FUNCT_2:52;

then A23: j in Seg (N + 1) by A1, A2, A22, FUNCT_1:def 3;

A24: rng R9 = Seg n by FUNCT_2:def 3;

dom R9 = Seg n by FUNCT_2:52;

then A25: (Rem (p1,i)) . k in Seg n by A20, A24, FUNCT_1:def 3;

then consider Rk being Nat such that

A26: Rk = (Rem (p1,i)) . k and

1 <= Rk and

Rk <= n ;

A27: (N + 1) -' 1 = (N + 1) - 1 by XREAL_0:def 2;

n <= N + 1 by NAT_1:11;

then A28: Seg n c= Seg (N + 1) by FINSEQ_1:5;

thus ( k < i implies (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . k ) :: thesis: ( k >= i implies (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . (k + 1) )

assume A31: k >= i ; :: thesis: (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . (k + 1)

then k1 > i by NAT_1:13;

then p19 . k1 <> p19 . i by A1, A21, A30, FUNCT_1:def 4;

then ( p1 . k1 < j or p1 . k1 > j ) by A2, XXREAL_0:1;

then ( ( Rk = p1 . k1 & p1 . k1 < j ) or ( p1 . k1 > j & Rk = (p1 . k1) - 1 ) ) by A1, A2, A20, A26, A31, Def3;

then ( ( Rk = p1 . k1 & p1 . k1 < j ) or ( p1 . k1 > j & p1 . k1 = Rk + 1 ) ) ;

then ( ( Rk = p1 . k1 & p1 . k1 < j ) or ( p1 . k1 > j & Rk >= j & p1 . k1 = Rk + 1 ) ) by NAT_1:13;

then ( ( DM * (k,Rk) = M * ((k + 1),Rk) & (Path_matrix ((Rem (p1,i)),DM)) . k = DM * (k,Rk) & (Path_matrix (p1,M)) . k1 = M * ((k + 1),Rk) ) or ( (Path_matrix ((Rem (p1,i)),DM)) . k = DM * (k,Rk) & DM * (k,Rk) = M * ((k + 1),(Rk + 1)) & (Path_matrix (p1,M)) . k1 = M * (k1,(Rk + 1)) ) ) by A1, A3, A20, A25, A23, A26, A27, A21, A19, A18, A31, Th13, MATRIX_3:def 7;

hence (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . (k + 1) ; :: thesis: verum

end;then A18: dom (Path_matrix (p1,M)) = Seg (N + 1) by FINSEQ_1:def 3;

len (Path_matrix ((Rem (p1,i)),DM)) = n by MATRIX_3:def 7;

then A19: dom (Path_matrix ((Rem (p1,i)),DM)) = Seg n by FINSEQ_1:def 3;

reconsider p19 = p1 as Permutation of (Seg (N + 1)) by MATRIX_1:def 12;

reconsider R9 = Rem (p1,i) as Permutation of (Seg n) by MATRIX_1:def 12;

let k be Nat; :: thesis: ( k in Seg n implies ( ( k < i implies (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . k ) & ( k >= i implies (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . (k + 1) ) ) )

assume A20: k in Seg n ; :: thesis: ( ( k < i implies (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . k ) & ( k >= i implies (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . (k + 1) ) )

reconsider k1 = k + 1 as Element of NAT ;

A21: k1 in Seg (N + 1) by A20, FINSEQ_1:60;

A22: rng p19 = Seg (N + 1) by FUNCT_2:def 3;

dom p19 = Seg (N + 1) by FUNCT_2:52;

then A23: j in Seg (N + 1) by A1, A2, A22, FUNCT_1:def 3;

A24: rng R9 = Seg n by FUNCT_2:def 3;

dom R9 = Seg n by FUNCT_2:52;

then A25: (Rem (p1,i)) . k in Seg n by A20, A24, FUNCT_1:def 3;

then consider Rk being Nat such that

A26: Rk = (Rem (p1,i)) . k and

1 <= Rk and

Rk <= n ;

A27: (N + 1) -' 1 = (N + 1) - 1 by XREAL_0:def 2;

n <= N + 1 by NAT_1:11;

then A28: Seg n c= Seg (N + 1) by FINSEQ_1:5;

thus ( k < i implies (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . k ) :: thesis: ( k >= i implies (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . (k + 1) )

proof

A30:
dom p19 = Seg (N + 1)
by FUNCT_2:52;
assume A29:
k < i
; :: thesis: (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . k

dom p19 = Seg (N + 1) by FUNCT_2:52;

then p19 . k <> p19 . i by A1, A20, A28, A29, FUNCT_1:def 4;

then ( p1 . k < j or p1 . k > j ) by A2, XXREAL_0:1;

then ( ( Rk = p1 . k & p1 . k < j ) or ( p1 . k > j & Rk = (p1 . k) - 1 ) ) by A1, A2, A20, A26, A29, Def3;

then ( ( Rk = p1 . k & p1 . k < j ) or ( p1 . k > j & p1 . k = Rk + 1 ) ) ;

then ( ( Rk = p1 . k & p1 . k < j ) or ( p1 . k > j & Rk >= j & p1 . k = Rk + 1 ) ) by NAT_1:13;

then ( ( DM * (k,Rk) = M * (k,Rk) & (Path_matrix ((Rem (p1,i)),DM)) . k = DM * (k,Rk) & (Path_matrix (p1,M)) . k = M * (k,Rk) ) or ( (Path_matrix ((Rem (p1,i)),DM)) . k = DM * (k,Rk) & DM * (k,Rk) = M * (k,(Rk + 1)) & (Path_matrix (p1,M)) . k = M * (k,(Rk + 1)) ) ) by A1, A3, A20, A25, A23, A26, A28, A27, A19, A18, A29, Th13, MATRIX_3:def 7;

hence (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . k ; :: thesis: verum

end;dom p19 = Seg (N + 1) by FUNCT_2:52;

then p19 . k <> p19 . i by A1, A20, A28, A29, FUNCT_1:def 4;

then ( p1 . k < j or p1 . k > j ) by A2, XXREAL_0:1;

then ( ( Rk = p1 . k & p1 . k < j ) or ( p1 . k > j & Rk = (p1 . k) - 1 ) ) by A1, A2, A20, A26, A29, Def3;

then ( ( Rk = p1 . k & p1 . k < j ) or ( p1 . k > j & p1 . k = Rk + 1 ) ) ;

then ( ( Rk = p1 . k & p1 . k < j ) or ( p1 . k > j & Rk >= j & p1 . k = Rk + 1 ) ) by NAT_1:13;

then ( ( DM * (k,Rk) = M * (k,Rk) & (Path_matrix ((Rem (p1,i)),DM)) . k = DM * (k,Rk) & (Path_matrix (p1,M)) . k = M * (k,Rk) ) or ( (Path_matrix ((Rem (p1,i)),DM)) . k = DM * (k,Rk) & DM * (k,Rk) = M * (k,(Rk + 1)) & (Path_matrix (p1,M)) . k = M * (k,(Rk + 1)) ) ) by A1, A3, A20, A25, A23, A26, A28, A27, A19, A18, A29, Th13, MATRIX_3:def 7;

hence (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . k ; :: thesis: verum

assume A31: k >= i ; :: thesis: (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . (k + 1)

then k1 > i by NAT_1:13;

then p19 . k1 <> p19 . i by A1, A21, A30, FUNCT_1:def 4;

then ( p1 . k1 < j or p1 . k1 > j ) by A2, XXREAL_0:1;

then ( ( Rk = p1 . k1 & p1 . k1 < j ) or ( p1 . k1 > j & Rk = (p1 . k1) - 1 ) ) by A1, A2, A20, A26, A31, Def3;

then ( ( Rk = p1 . k1 & p1 . k1 < j ) or ( p1 . k1 > j & p1 . k1 = Rk + 1 ) ) ;

then ( ( Rk = p1 . k1 & p1 . k1 < j ) or ( p1 . k1 > j & Rk >= j & p1 . k1 = Rk + 1 ) ) by NAT_1:13;

then ( ( DM * (k,Rk) = M * ((k + 1),Rk) & (Path_matrix ((Rem (p1,i)),DM)) . k = DM * (k,Rk) & (Path_matrix (p1,M)) . k1 = M * ((k + 1),Rk) ) or ( (Path_matrix ((Rem (p1,i)),DM)) . k = DM * (k,Rk) & DM * (k,Rk) = M * ((k + 1),(Rk + 1)) & (Path_matrix (p1,M)) . k1 = M * (k1,(Rk + 1)) ) ) by A1, A3, A20, A25, A23, A26, A27, A21, A19, A18, A31, Th13, MATRIX_3:def 7;

hence (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . (k + 1) ; :: thesis: verum

S

proof

defpred S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A33: S_{1}[k]
; :: thesis: S_{1}[k + 1]

reconsider e = k as Element of NAT by ORDINAL1:def 12;

assume that

A34: 1 <= k + 1 and

A35: k + 1 < i ; :: thesis: f . (k + 1) = F . (k + 1)

set k1 = e + 1;

i <= N + 1 by A1, FINSEQ_1:1;

then e + 1 < N + 1 by A35, XXREAL_0:2;

then e + 1 <= n by NAT_1:13;

then A36: e + 1 in Seg N by A34;

end;assume A33: S

reconsider e = k as Element of NAT by ORDINAL1:def 12;

assume that

A34: 1 <= k + 1 and

A35: k + 1 < i ; :: thesis: f . (k + 1) = F . (k + 1)

set k1 = e + 1;

i <= N + 1 by A1, FINSEQ_1:1;

then e + 1 < N + 1 by A35, XXREAL_0:2;

then e + 1 <= n by NAT_1:13;

then A36: e + 1 in Seg N by A34;

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

end;

suppose A37:
k >= 1
; :: thesis: f . (k + 1) = F . (k + 1)

i <= N + 1
by A1, FINSEQ_1:1;

then A38: e + 1 < N + 1 by A35, XXREAL_0:2;

then k < N + 1 by NAT_1:13;

then A39: F . (e + 1) = the multF of K . ((F . k),((Path_matrix (p1,M)) . (e + 1))) by A15, A37;

e + 1 <= n by A38, NAT_1:13;

then A40: e + 1 in Seg N by A34;

k < n by A38, XREAL_1:6;

then f . (e + 1) = the multF of K . ((f . k),((Path_matrix ((Rem (p1,i)),DM)) . (e + 1))) by A12, A37;

hence f . (k + 1) = F . (k + 1) by A17, A33, A35, A37, A39, A40, NAT_1:13; :: thesis: verum

end;then A38: e + 1 < N + 1 by A35, XXREAL_0:2;

then k < N + 1 by NAT_1:13;

then A39: F . (e + 1) = the multF of K . ((F . k),((Path_matrix (p1,M)) . (e + 1))) by A15, A37;

e + 1 <= n by A38, NAT_1:13;

then A40: e + 1 in Seg N by A34;

k < n by A38, XREAL_1:6;

then f . (e + 1) = the multF of K . ((f . k),((Path_matrix ((Rem (p1,i)),DM)) . (e + 1))) by A12, A37;

hence f . (k + 1) = F . (k + 1) by A17, A33, A35, A37, A39, A40, NAT_1:13; :: thesis: verum

F . $1 = (M * (i,j)) * a ) ) );

A41: S

A42: for k being Nat holds S

A43: for k being Nat st S

S

proof

A63:
S
let k be Nat; :: thesis: ( S_{2}[k] implies S_{2}[k + 1] )

assume A44: S_{2}[k]
; :: thesis: S_{2}[k + 1]

set k1 = k + 1;

assume that

A45: i <= k + 1 and

A46: k + 1 <= N + 1 ; :: thesis: ( ( k + 1 = 1 implies F . (k + 1) = M * (i,j) ) & ( k + 1 > 1 implies for a being Element of K st a = f . ((k + 1) - 1) holds

F . (k + 1) = (M * (i,j)) * a ) )

end;assume A44: S

set k1 = k + 1;

assume that

A45: i <= k + 1 and

A46: k + 1 <= N + 1 ; :: thesis: ( ( k + 1 = 1 implies F . (k + 1) = M * (i,j) ) & ( k + 1 > 1 implies for a being Element of K st a = f . ((k + 1) - 1) holds

F . (k + 1) = (M * (i,j)) * a ) )

per cases
( k = 0 or k > 0 )
;

end;

suppose A47:
k = 0
; :: thesis: ( ( k + 1 = 1 implies F . (k + 1) = M * (i,j) ) & ( k + 1 > 1 implies for a being Element of K st a = f . ((k + 1) - 1) holds

F . (k + 1) = (M * (i,j)) * a ) )

F . (k + 1) = (M * (i,j)) * a ) )

1 <= i
by A1, FINSEQ_1:1;

hence ( ( k + 1 = 1 implies F . (k + 1) = M * (i,j) ) & ( k + 1 > 1 implies for a being Element of K st a = f . ((k + 1) - 1) holds

F . (k + 1) = (M * (i,j)) * a ) ) by A4, A14, A45, A47, XXREAL_0:1; :: thesis: verum

end;hence ( ( k + 1 = 1 implies F . (k + 1) = M * (i,j) ) & ( k + 1 > 1 implies for a being Element of K st a = f . ((k + 1) - 1) holds

F . (k + 1) = (M * (i,j)) * a ) ) by A4, A14, A45, A47, XXREAL_0:1; :: thesis: verum

suppose A48:
k > 0
; :: thesis: ( ( k + 1 = 1 implies F . (k + 1) = M * (i,j) ) & ( k + 1 > 1 implies for a being Element of K st a = f . ((k + 1) - 1) holds

F . (k + 1) = (M * (i,j)) * a ) )

F . (k + 1) = (M * (i,j)) * a ) )

hence
( k + 1 = 1 implies F . (k + 1) = M * (i,j) )
; :: thesis: ( k + 1 > 1 implies for a being Element of K st a = f . ((k + 1) - 1) holds

F . (k + 1) = (M * (i,j)) * a )

assume k + 1 > 1 ; :: thesis: for a being Element of K st a = f . ((k + 1) - 1) holds

F . (k + 1) = (M * (i,j)) * a

let a be Element of K; :: thesis: ( a = f . ((k + 1) - 1) implies F . (k + 1) = (M * (i,j)) * a )

assume A49: a = f . ((k + 1) - 1) ; :: thesis: F . (k + 1) = (M * (i,j)) * a

A50: k <= n by A46, XREAL_1:6;

k >= 1 by A48, NAT_1:14;

then A51: k in Seg n by A50;

len (Path_matrix ((Rem (p1,i)),DM)) = n by MATRIX_3:def 7;

then A52: dom (Path_matrix ((Rem (p1,i)),DM)) = Seg n by FINSEQ_1:def 3;

then A53: (Path_matrix ((Rem (p1,i)),DM)) . k = DM * (k,((Rem (p1,i)) . k)) by A51, MATRIX_3:def 7;

k < N + 1 by A46, NAT_1:13;

then A54: F . (k + 1) = the multF of K . ((F . k),((Path_matrix (p1,M)) . (k + 1))) by A15, A48;

end;F . (k + 1) = (M * (i,j)) * a )

assume k + 1 > 1 ; :: thesis: for a being Element of K st a = f . ((k + 1) - 1) holds

F . (k + 1) = (M * (i,j)) * a

let a be Element of K; :: thesis: ( a = f . ((k + 1) - 1) implies F . (k + 1) = (M * (i,j)) * a )

assume A49: a = f . ((k + 1) - 1) ; :: thesis: F . (k + 1) = (M * (i,j)) * a

A50: k <= n by A46, XREAL_1:6;

k >= 1 by A48, NAT_1:14;

then A51: k in Seg n by A50;

len (Path_matrix ((Rem (p1,i)),DM)) = n by MATRIX_3:def 7;

then A52: dom (Path_matrix ((Rem (p1,i)),DM)) = Seg n by FINSEQ_1:def 3;

then A53: (Path_matrix ((Rem (p1,i)),DM)) . k = DM * (k,((Rem (p1,i)) . k)) by A51, MATRIX_3:def 7;

k < N + 1 by A46, NAT_1:13;

then A54: F . (k + 1) = the multF of K . ((F . k),((Path_matrix (p1,M)) . (k + 1))) by A15, A48;

per cases
( k + 1 = i or k + 1 > i )
by A45, XXREAL_0:1;

end;

suppose A55:
k + 1 = i
; :: thesis: F . (k + 1) = (M * (i,j)) * a

then
k < i
by NAT_1:13;

then F . (k + 1) = a * (M * (i,j)) by A4, A42, A48, A49, A54, A55, NAT_1:14;

hence F . (k + 1) = (M * (i,j)) * a ; :: thesis: verum

end;then F . (k + 1) = a * (M * (i,j)) by A4, A42, A48, A49, A54, A55, NAT_1:14;

hence F . (k + 1) = (M * (i,j)) * a ; :: thesis: verum

suppose A56:
k + 1 > i
; :: thesis: F . (k + 1) = (M * (i,j)) * a

A57:
k < N + 1
by A46, NAT_1:13;

A58: k >= i by A56, NAT_1:13;

i >= 1 by A1, FINSEQ_1:1;

then A59: k >= 1 by A58, XXREAL_0:2;

end;A58: k >= i by A56, NAT_1:13;

i >= 1 by A1, FINSEQ_1:1;

then A59: k >= 1 by A58, XXREAL_0:2;

per cases
( k = 1 or k > 1 )
by A59, XXREAL_0:1;

end;

suppose
k = 1
; :: thesis: F . (k + 1) = (M * (i,j)) * a

hence
F . (k + 1) = (M * (i,j)) * a
by A11, A17, A44, A46, A49, A51, A54, A58, NAT_1:13; :: thesis: verum

end;suppose A60:
k > 1
; :: thesis: F . (k + 1) = (M * (i,j)) * a

reconsider k9 = k - 1 as Element of NAT by A48, NAT_1:20;

reconsider fk9 = f . k9 as Element of K ;

k9 + 1 <= n by A57, NAT_1:13;

then A61: k9 < n by NAT_1:13;

k9 + 1 > 0 + 1 by A60;

then A62: a = the multF of K . (fk9,((Path_matrix ((Rem (p1,i)),DM)) . (k9 + 1))) by A12, A49, A61;

F . k = (M * (i,j)) * fk9 by A44, A46, A56, A60, NAT_1:13;

hence F . (k + 1) = ((M * (i,j)) * fk9) * (DM * (k,((Rem (p1,i)) . k))) by A17, A51, A54, A53, A58

.= (M * (i,j)) * (fk9 * (DM * (k,((Rem (p1,i)) . k)))) by GROUP_1:def 3

.= (M * (i,j)) * a by A51, A52, A62, MATRIX_3:def 7 ;

:: thesis: verum

end;reconsider fk9 = f . k9 as Element of K ;

k9 + 1 <= n by A57, NAT_1:13;

then A61: k9 < n by NAT_1:13;

k9 + 1 > 0 + 1 by A60;

then A62: a = the multF of K . (fk9,((Path_matrix ((Rem (p1,i)),DM)) . (k9 + 1))) by A12, A49, A61;

F . k = (M * (i,j)) * fk9 by A44, A46, A56, A60, NAT_1:13;

hence F . (k + 1) = ((M * (i,j)) * fk9) * (DM * (k,((Rem (p1,i)) . k))) by A17, A51, A54, A53, A58

.= (M * (i,j)) * (fk9 * (DM * (k,((Rem (p1,i)) . k)))) by GROUP_1:def 3

.= (M * (i,j)) * a by A51, A52, A62, MATRIX_3:def 7 ;

:: thesis: verum

A64: for k being Nat holds S

A65: i <= N + 1 by A1, FINSEQ_1:1;

A66: (N + 1) - 1 = n ;

N + 1 > 0 + 1 by A10, XREAL_1:6;

hence the multF of K $$ (Path_matrix (p1,M)) = (M * (i,j)) * ( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM))) by A16, A13, A64, A65, A66; :: thesis: verum

per cases
( Rem (p1,i) is even or Rem (p1,i) is odd )
;

end;

suppose A67:
Rem (p1,i) is even
; :: thesis: (Path_product M) . p1 = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i)))

thus (Path_product M) . p1 =
- (( the multF of K $$ (Path_matrix (p1,M))),p1)
by MATRIX_3:def 8

.= ((power K) . ((- (1_ K)),(i + j))) * (- (( the multF of K $$ (Path_matrix (p1,M))),(Rem (p1,i)))) by A1, A2, Th21

.= ((power K) . ((- (1_ K)),(i + j))) * ((M * (i,j)) * ( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM)))) by A5, A67, MATRIX_1:def 16

.= (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM))) by GROUP_1:def 3

.= (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * (- (( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM))),(Rem (p1,i)))) by A67, MATRIX_1:def 16

.= (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i))) by MATRIX_3:def 8 ; :: thesis: verum

end;.= ((power K) . ((- (1_ K)),(i + j))) * (- (( the multF of K $$ (Path_matrix (p1,M))),(Rem (p1,i)))) by A1, A2, Th21

.= ((power K) . ((- (1_ K)),(i + j))) * ((M * (i,j)) * ( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM)))) by A5, A67, MATRIX_1:def 16

.= (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM))) by GROUP_1:def 3

.= (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * (- (( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM))),(Rem (p1,i)))) by A67, MATRIX_1:def 16

.= (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i))) by MATRIX_3:def 8 ; :: thesis: verum

suppose A68:
Rem (p1,i) is odd
; :: thesis: (Path_product M) . p1 = (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i)))

thus (Path_product M) . p1 =
- (( the multF of K $$ (Path_matrix (p1,M))),p1)
by MATRIX_3:def 8

.= ((power K) . ((- (1_ K)),(i + j))) * (- (( the multF of K $$ (Path_matrix (p1,M))),(Rem (p1,i)))) by A1, A2, Th21

.= ((power K) . ((- (1_ K)),(i + j))) * (- ((M * (i,j)) * ( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM))))) by A5, A68, MATRIX_1:def 16

.= ((power K) . ((- (1_ K)),(i + j))) * ((M * (i,j)) * (- ( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM))))) by VECTSP_1:8

.= (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * (- ( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM)))) by GROUP_1:def 3

.= (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * (- (( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM))),(Rem (p1,i)))) by A68, MATRIX_1:def 16

.= (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i))) by MATRIX_3:def 8 ; :: thesis: verum

end;.= ((power K) . ((- (1_ K)),(i + j))) * (- (( the multF of K $$ (Path_matrix (p1,M))),(Rem (p1,i)))) by A1, A2, Th21

.= ((power K) . ((- (1_ K)),(i + j))) * (- ((M * (i,j)) * ( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM))))) by A5, A68, MATRIX_1:def 16

.= ((power K) . ((- (1_ K)),(i + j))) * ((M * (i,j)) * (- ( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM))))) by VECTSP_1:8

.= (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * (- ( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM)))) by GROUP_1:def 3

.= (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * (- (( the multF of K $$ (Path_matrix ((Rem (p1,i)),DM))),(Rem (p1,i)))) by A68, MATRIX_1:def 16

.= (((power K) . ((- (1_ K)),(i + j))) * (M * (i,j))) * ((Path_product DM) . (Rem (p1,i))) by MATRIX_3:def 8 ; :: thesis: verum