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
() . p1 = ((() . ((- (1_ K)),(i + j))) * (M * (i,j))) * (() . (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
() . p1 = ((() . ((- (1_ K)),(i + j))) * (M * (i,j))) * (() . (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
() . p1 = ((() . ((- (1_ K)),(i + j))) * (M * (i,j))) * (() . (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
() . p1 = ((() . ((- (1_ K)),(i + j))) * (M * (i,j))) * (() . (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
() . p1 = ((() . ((- (1_ K)),(i + j))) * (M * (i,j))) * (() . (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
() . p1 = ((() . ((- (1_ K)),(i + j))) * (M * (i,j))) * (() . (Rem (p1,i)))

let DM be Matrix of n,K; :: thesis: ( DM = Delete (M,i,j) implies () . p1 = ((() . ((- (1_ K)),(i + j))) * (M * (i,j))) * (() . (Rem (p1,i))) )
assume A3: DM = Delete (M,i,j) ; :: thesis: () . p1 = ((() . ((- (1_ K)),(i + j))) * (M * (i,j))) * (() . (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 ;
A5: now :: thesis: the multF of K \$\$ (Path_matrix (p1,M)) = (M * (i,j)) * ( the multF of K \$\$ (Path_matrix ((Rem (p1,i)),DM)))
per cases ( N = 0 or N > 0 ) ;
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 ;
then Path_matrix (p1,M) = <*(M * (i,j))*> by ;
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 ;
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;
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 ;
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 S1[ 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) ) )
proof
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 ;
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 ;
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 ;
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
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 ;
then ( p1 . k < j or p1 . k > j ) by ;
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 ;
hence (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . k ; :: thesis: verum
end;
A30: dom p19 = Seg (N + 1) by FUNCT_2:52;
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 ;
then ( p1 . k1 < j or p1 . k1 > j ) by ;
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 ;
hence (Path_matrix ((Rem (p1,i)),DM)) . k = (Path_matrix (p1,M)) . (k + 1) ; :: thesis: verum
end;
A32: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A33: S1[k] ; :: thesis: S1[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 ;
then e + 1 < N + 1 by ;
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;
suppose k = 0 ; :: thesis: f . (k + 1) = F . (k + 1)
hence f . (k + 1) = F . (k + 1) by A14, A11, A17, A35, A36; :: thesis: verum
end;
suppose A37: k >= 1 ; :: thesis: f . (k + 1) = F . (k + 1)
i <= N + 1 by ;
then A38: e + 1 < N + 1 by ;
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 ;
e + 1 <= n by ;
then A40: e + 1 in Seg N by A34;
k < n by ;
then f . (e + 1) = the multF of K . ((f . k),((Path_matrix ((Rem (p1,i)),DM)) . (e + 1))) by ;
hence f . (k + 1) = F . (k + 1) by ; :: thesis: verum
end;
end;
end;
defpred S2[ 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: S1[ 0 ] ;
A42: for k being Nat holds S1[k] from A43: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A44: S2[k] ; :: thesis: S2[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 ) )

per cases ( k = 0 or k > 0 ) ;
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 ) )

1 <= i by ;
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 ; :: thesis: verum
end;
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 ) )

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 ;
k >= 1 by ;
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 ;
k < N + 1 by ;
then A54: F . (k + 1) = the multF of K . ((F . k),((Path_matrix (p1,M)) . (k + 1))) by ;
per cases ( k + 1 = i or k + 1 > i ) by ;
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 ;
hence F . (k + 1) = (M * (i,j)) * a ; :: thesis: verum
end;
suppose A56: k + 1 > i ; :: thesis: F . (k + 1) = (M * (i,j)) * a
A57: k < N + 1 by ;
A58: k >= i by ;
i >= 1 by ;
then A59: k >= 1 by ;
per cases ( k = 1 or k > 1 ) by ;
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 ;
reconsider fk9 = f . k9 as Element of K ;
k9 + 1 <= n by ;
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 ;
F . k = (M * (i,j)) * fk9 by ;
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 ;
:: thesis: verum
end;
end;
end;
end;
end;
end;
end;
A63: S2[ 0 ] ;
A64: for k being Nat holds S2[k] from A65: i <= N + 1 by ;
A66: (N + 1) - 1 = n ;
N + 1 > 0 + 1 by ;
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;
end;
end;
per cases ( Rem (p1,i) is even or Rem (p1,i) is odd ) ;
suppose A67: Rem (p1,i) is even ; :: thesis: () . p1 = ((() . ((- (1_ K)),(i + j))) * (M * (i,j))) * (() . (Rem (p1,i)))
thus () . p1 = - (( the multF of K \$\$ (Path_matrix (p1,M))),p1) by MATRIX_3:def 8
.= (() . ((- (1_ K)),(i + j))) * (- (( the multF of K \$\$ (Path_matrix (p1,M))),(Rem (p1,i)))) by A1, A2, Th21
.= (() . ((- (1_ K)),(i + j))) * ((M * (i,j)) * ( the multF of K \$\$ (Path_matrix ((Rem (p1,i)),DM)))) by
.= ((() . ((- (1_ K)),(i + j))) * (M * (i,j))) * ( the multF of K \$\$ (Path_matrix ((Rem (p1,i)),DM))) by GROUP_1:def 3
.= ((() . ((- (1_ K)),(i + j))) * (M * (i,j))) * (- (( the multF of K \$\$ (Path_matrix ((Rem (p1,i)),DM))),(Rem (p1,i)))) by
.= ((() . ((- (1_ K)),(i + j))) * (M * (i,j))) * (() . (Rem (p1,i))) by MATRIX_3:def 8 ; :: thesis: verum
end;
suppose A68: Rem (p1,i) is odd ; :: thesis: () . p1 = ((() . ((- (1_ K)),(i + j))) * (M * (i,j))) * (() . (Rem (p1,i)))
thus () . p1 = - (( the multF of K \$\$ (Path_matrix (p1,M))),p1) by MATRIX_3:def 8
.= (() . ((- (1_ K)),(i + j))) * (- (( the multF of K \$\$ (Path_matrix (p1,M))),(Rem (p1,i)))) by A1, A2, Th21
.= (() . ((- (1_ K)),(i + j))) * (- ((M * (i,j)) * ( the multF of K \$\$ (Path_matrix ((Rem (p1,i)),DM))))) by
.= (() . ((- (1_ K)),(i + j))) * ((M * (i,j)) * (- ( the multF of K \$\$ (Path_matrix ((Rem (p1,i)),DM))))) by VECTSP_1:8
.= ((() . ((- (1_ K)),(i + j))) * (M * (i,j))) * (- ( the multF of K \$\$ (Path_matrix ((Rem (p1,i)),DM)))) by GROUP_1:def 3
.= ((() . ((- (1_ K)),(i + j))) * (M * (i,j))) * (- (( the multF of K \$\$ (Path_matrix ((Rem (p1,i)),DM))),(Rem (p1,i)))) by
.= ((() . ((- (1_ K)),(i + j))) * (M * (i,j))) * (() . (Rem (p1,i))) by MATRIX_3:def 8 ; :: thesis: verum
end;
end;