theorem :: MATRIX12:23

for l, n being Nat
for K being Field
for a being Element of K st l in dom (1. (K,n)) & a <> 0. K & n > 0 holds
(SXCol ((1. (K,n)),l,a)) ~ = SXCol ((1. (K,n)),l,(a "))