theorem :: MATRIX_9:56

for n being Nat
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) )