let n be Nat; :: thesis: for K being Field

for a being Element of K

for M, N being Matrix of n,K st ex i being Element of NAT st

( i in Seg n & ( for k being Element of NAT st k in Seg n holds

(Col (M,i)) . k = a * ((Col (N,i)) /. k) ) & ( for l being Element of NAT st l <> i & l in Seg n holds

Col (M,l) = Col (N,l) ) ) holds

for p being Element of Permutations n ex l being Element of NAT st

( l in Seg n & (Path_matrix (p,M)) /. l = a * ((Path_matrix (p,N)) /. l) )

let K be Field; :: thesis: for a being Element of K

for M, N being Matrix of n,K st ex i being Element of NAT st

( i in Seg n & ( for k being Element of NAT st k in Seg n holds

(Col (M,i)) . k = a * ((Col (N,i)) /. k) ) & ( for l being Element of NAT st l <> i & l in Seg n holds

Col (M,l) = Col (N,l) ) ) holds

for p being Element of Permutations n ex l being Element of NAT st

( l in Seg n & (Path_matrix (p,M)) /. l = a * ((Path_matrix (p,N)) /. l) )

let a be Element of K; :: thesis: for M, N being Matrix of n,K st ex i being Element of NAT st

( i in Seg n & ( for k being Element of NAT st k in Seg n holds

(Col (M,i)) . k = a * ((Col (N,i)) /. k) ) & ( for l being Element of NAT st l <> i & l in Seg n holds

Col (M,l) = Col (N,l) ) ) holds

for p being Element of Permutations n ex l being Element of NAT st

( l in Seg n & (Path_matrix (p,M)) /. l = a * ((Path_matrix (p,N)) /. l) )

let M, N be Matrix of n,K; :: thesis: ( ex i being Element of NAT st

( i in Seg n & ( for k being Element of NAT st k in Seg n holds

(Col (M,i)) . k = a * ((Col (N,i)) /. k) ) & ( for l being Element of NAT st l <> i & l in Seg n holds

Col (M,l) = Col (N,l) ) ) implies for p being Element of Permutations n ex l being Element of NAT st

( l in Seg n & (Path_matrix (p,M)) /. l = a * ((Path_matrix (p,N)) /. l) ) )

assume ex i being Element of NAT st

( i in Seg n & ( for k being Element of NAT st k in Seg n holds

(Col (M,i)) . k = a * ((Col (N,i)) /. k) ) & ( for l being Element of NAT st l <> i & l in Seg n holds

Col (M,l) = Col (N,l) ) ) ; :: thesis: for p being Element of Permutations n ex l being Element of NAT st

( l in Seg n & (Path_matrix (p,M)) /. l = a * ((Path_matrix (p,N)) /. l) )

then consider i being Element of NAT such that

A1: i in Seg n and

A2: for k being Element of NAT st k in Seg n holds

(Col (M,i)) . k = a * ((Col (N,i)) /. k) and

for l being Element of NAT st l <> i & l in Seg n holds

Col (M,l) = Col (N,l) ;

let p be Element of Permutations n; :: thesis: ex l being Element of NAT st

( l in Seg n & (Path_matrix (p,M)) /. l = a * ((Path_matrix (p,N)) /. l) )

n in NAT by ORDINAL1:def 12;

then consider k being Element of NAT such that

A3: k in Seg n and

A4: i = p . k by A1, Th48;

A5: 1 <= k by A3, FINSEQ_1:1;

len (Path_matrix (p,N)) = n by MATRIX_3:def 7;

then A6: k in dom (Path_matrix (p,N)) by A3, FINSEQ_1:def 3;

then (Path_matrix (p,N)) . k = N * (k,i) by A4, MATRIX_3:def 7;

then A7: (Path_matrix (p,N)) /. k = N * (k,i) by A6, PARTFUN1:def 6;

len (Col (N,i)) = len N by MATRIX_0:def 8;

then A8: dom (Col (N,i)) = dom N by FINSEQ_3:29;

len N = n by MATRIX_0:def 2;

then k <= len N by A3, FINSEQ_1:1;

then A9: k in dom N by A5, FINSEQ_3:25;

then (Col (N,i)) . k = N * (k,i) by MATRIX_0:def 8;

then A10: (Col (N,i)) /. k = (Path_matrix (p,N)) /. k by A9, A7, A8, PARTFUN1:def 6;

len M = n by MATRIX_0:def 2;

then k <= len M by A3, FINSEQ_1:1;

then A11: k in dom M by A5, FINSEQ_3:25;

take k ; :: thesis: ( k in Seg n & (Path_matrix (p,M)) /. k = a * ((Path_matrix (p,N)) /. k) )

len (Path_matrix (p,M)) = n by MATRIX_3:def 7;

then A12: dom (Path_matrix (p,M)) = Seg n by FINSEQ_1:def 3;

then (Path_matrix (p,M)) . k = M * (k,i) by A3, A4, MATRIX_3:def 7;

then (Path_matrix (p,M)) . k = (Col (M,i)) . k by A11, MATRIX_0:def 8

.= a * ((Path_matrix (p,N)) /. k) by A2, A3, A10 ;

hence ( k in Seg n & (Path_matrix (p,M)) /. k = a * ((Path_matrix (p,N)) /. k) ) by A12, A3, PARTFUN1:def 6; :: thesis: verum

for a being Element of K

for M, N being Matrix of n,K st ex i being Element of NAT st

( i in Seg n & ( for k being Element of NAT st k in Seg n holds

(Col (M,i)) . k = a * ((Col (N,i)) /. k) ) & ( for l being Element of NAT st l <> i & l in Seg n holds

Col (M,l) = Col (N,l) ) ) holds

for p being Element of Permutations n ex l being Element of NAT st

( l in Seg n & (Path_matrix (p,M)) /. l = a * ((Path_matrix (p,N)) /. l) )

let K be Field; :: thesis: for a being Element of K

for M, N being Matrix of n,K st ex i being Element of NAT st

( i in Seg n & ( for k being Element of NAT st k in Seg n holds

(Col (M,i)) . k = a * ((Col (N,i)) /. k) ) & ( for l being Element of NAT st l <> i & l in Seg n holds

Col (M,l) = Col (N,l) ) ) holds

for p being Element of Permutations n ex l being Element of NAT st

( l in Seg n & (Path_matrix (p,M)) /. l = a * ((Path_matrix (p,N)) /. l) )

let a be Element of K; :: thesis: for M, N being Matrix of n,K st ex i being Element of NAT st

( i in Seg n & ( for k being Element of NAT st k in Seg n holds

(Col (M,i)) . k = a * ((Col (N,i)) /. k) ) & ( for l being Element of NAT st l <> i & l in Seg n holds

Col (M,l) = Col (N,l) ) ) holds

for p being Element of Permutations n ex l being Element of NAT st

( l in Seg n & (Path_matrix (p,M)) /. l = a * ((Path_matrix (p,N)) /. l) )

let M, N be Matrix of n,K; :: thesis: ( ex i being Element of NAT st

( i in Seg n & ( for k being Element of NAT st k in Seg n holds

(Col (M,i)) . k = a * ((Col (N,i)) /. k) ) & ( for l being Element of NAT st l <> i & l in Seg n holds

Col (M,l) = Col (N,l) ) ) implies for p being Element of Permutations n ex l being Element of NAT st

( l in Seg n & (Path_matrix (p,M)) /. l = a * ((Path_matrix (p,N)) /. l) ) )

assume ex i being Element of NAT st

( i in Seg n & ( for k being Element of NAT st k in Seg n holds

(Col (M,i)) . k = a * ((Col (N,i)) /. k) ) & ( for l being Element of NAT st l <> i & l in Seg n holds

Col (M,l) = Col (N,l) ) ) ; :: thesis: for p being Element of Permutations n ex l being Element of NAT st

( l in Seg n & (Path_matrix (p,M)) /. l = a * ((Path_matrix (p,N)) /. l) )

then consider i being Element of NAT such that

A1: i in Seg n and

A2: for k being Element of NAT st k in Seg n holds

(Col (M,i)) . k = a * ((Col (N,i)) /. k) and

for l being Element of NAT st l <> i & l in Seg n holds

Col (M,l) = Col (N,l) ;

let p be Element of Permutations n; :: thesis: ex l being Element of NAT st

( l in Seg n & (Path_matrix (p,M)) /. l = a * ((Path_matrix (p,N)) /. l) )

n in NAT by ORDINAL1:def 12;

then consider k being Element of NAT such that

A3: k in Seg n and

A4: i = p . k by A1, Th48;

A5: 1 <= k by A3, FINSEQ_1:1;

len (Path_matrix (p,N)) = n by MATRIX_3:def 7;

then A6: k in dom (Path_matrix (p,N)) by A3, FINSEQ_1:def 3;

then (Path_matrix (p,N)) . k = N * (k,i) by A4, MATRIX_3:def 7;

then A7: (Path_matrix (p,N)) /. k = N * (k,i) by A6, PARTFUN1:def 6;

len (Col (N,i)) = len N by MATRIX_0:def 8;

then A8: dom (Col (N,i)) = dom N by FINSEQ_3:29;

len N = n by MATRIX_0:def 2;

then k <= len N by A3, FINSEQ_1:1;

then A9: k in dom N by A5, FINSEQ_3:25;

then (Col (N,i)) . k = N * (k,i) by MATRIX_0:def 8;

then A10: (Col (N,i)) /. k = (Path_matrix (p,N)) /. k by A9, A7, A8, PARTFUN1:def 6;

len M = n by MATRIX_0:def 2;

then k <= len M by A3, FINSEQ_1:1;

then A11: k in dom M by A5, FINSEQ_3:25;

take k ; :: thesis: ( k in Seg n & (Path_matrix (p,M)) /. k = a * ((Path_matrix (p,N)) /. k) )

len (Path_matrix (p,M)) = n by MATRIX_3:def 7;

then A12: dom (Path_matrix (p,M)) = Seg n by FINSEQ_1:def 3;

then (Path_matrix (p,M)) . k = M * (k,i) by A3, A4, MATRIX_3:def 7;

then (Path_matrix (p,M)) . k = (Col (M,i)) . k by A11, MATRIX_0:def 8

.= a * ((Path_matrix (p,N)) /. k) by A2, A3, A10 ;

hence ( k in Seg n & (Path_matrix (p,M)) /. k = a * ((Path_matrix (p,N)) /. k) ) by A12, A3, PARTFUN1:def 6; :: thesis: verum