theorem :: MATRIX12:23

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)) & n > 0 holds
(SXCol ((1. (K,n)),l,a)) ~ = SXCol ((1. (K,n)),l,(/ a))