let n be Nat; :: thesis:
let K be Field; :: thesis:
let a be Element of K; :: thesis:
let M, N be Matrix of n,K; :: thesis:
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:
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) ) & ( 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:
( len (Path_matrix p,M) = n & len (Path_matrix p,N) = n ) by MATRIX_3:def 7;
then A3: ( dom (Path_matrix p,M) = Seg n & dom (Path_matrix p,N) = Seg n ) by FINSEQ_1:def 3;
n in NAT by ORDINAL1:def 13;
then consider k being Element of NAT such that
A4: k in Seg n and
A5: i = p . k by A1, Th48;
( len M = n & len N = n ) by MATRIX_1:def 3;
then ( 1 <= k & k <= len M & 1 <= k & k <= len N ) by A4, FINSEQ_1:3;
then A6: ( k in dom M & k in dom N ) by FINSEQ_3:27;
then A7: ( (Col M,i) . k = M * k,i & (Col N,i) . k = N * k,i ) by MATRIX_1:def 9;
A8: (Col N,i) /. k = (Path_matrix p,N) /. k

len (Path_matrix p,N) = n by MATRIX_3:def 7;
then A9: k in dom (Path_matrix p,N) by A4, FINSEQ_1:def 3;
then (Path_matrix p,N) . k = N * k,i by A5, MATRIX_3:def 7;
then A10: (Path_matrix p,N) /. k = N * k,i by A9, PARTFUN1:def 8;
len (Col N,i) = len N by MATRIX_1:def 9;
then dom (Col N,i) = dom N by FINSEQ_3:31;
hence (Col N,i) /. k = (Path_matrix p,N) /. k by A6, A7, A10, PARTFUN1:def 8; :: thesis:

end;

( (Path_matrix p,M) . k = M * k,i & (Path_matrix p,N) . k = N * k,i ) by A3, A4, A5, MATRIX_3:def 7;
then A11: (Path_matrix p,M) . k = (Col M,i) . k by A6, MATRIX_1:def 9
.= a * ((Path_matrix p,N) /. k) by A2, A4, A8 ;
take k ; :: thesis:
thus ( k in Seg n & (Path_matrix p,M) /. k = a * ((Path_matrix p,N) /. k) ) by A3, A4, A11, PARTFUN1:def 8; :: thesis: