theorem Th54: :: MATRIX14:54

for n being Element of NAT
for K being Field
for A, B being Matrix of n,K st B * A = 1. (K,n) holds
ex B2 being Matrix of n,K st A * B2 = 1. (K,n)