theorem Th37: :: MATRIX14:37

for n being Element of NAT
for K being Field
for a being Element of K
for P, Q being Matrix of n,K st n > 0 & a <> 0. K & P * (1,1) = a " & ( for i being Element of NAT st 1 < i & i <= n holds
P . i = Base_FinSeq (K,n,i) ) & Q * (1,1) = a & ( for j being Element of NAT st 1 < j & j <= n holds
Q * (1,j) = - (a * (P * (1,j))) ) & ( for i being Element of NAT st 1 < i & i <= n holds
Q . i = Base_FinSeq (K,n,i) ) holds
( P is invertible & Q = P ~ )