theorem Th13:
for
k,
l,
n being
Nat for
K being
comRing 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)) )