for k, l, n being Nat
for K being Field
for a being Element of K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & k <> l holds
( RLineXS ((1. (K,n)),l,k,a) is invertible & (RLineXS ((1. (K,n)),l,k,a)) ~ = RLineXS ((1. (K,n)),l,k,(- a)) )