theorem Th14: :: MATRIX12:14

for l, n being Nat
for K being comRing
for a being Element of K st a is left_invertible & a is right_mult-cancelable & l in dom (1. (K,n)) holds
( SXLine ((1. (K,n)),l,a) is invertible & (SXLine ((1. (K,n)),l,a)) ~ = SXLine ((1. (K,n)),l,(/ a)) )