let k, l, n be Nat; :: thesis: 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)) )
let K be comRing; :: thesis: 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)) )
let a be Element of K; :: thesis: ( l in dom (1. (K,n)) & k in dom (1. (K,n)) & k <> l implies ( RLineXS ((1. (K,n)),l,k,a) is invertible & (RLineXS ((1. (K,n)),l,k,a)) ~ = RLineXS ((1. (K,n)),l,k,(- a)) ) )
assume that
A1: ( l in dom (1. (K,n)) & k in dom (1. (K,n)) ) and
A2: k <> l ; :: thesis: ( RLineXS ((1. (K,n)),l,k,a) is invertible & (RLineXS ((1. (K,n)),l,k,a)) ~ = RLineXS ((1. (K,n)),l,k,(- a)) )
set B = RLineXS ((1. (K,n)),l,k,(- a));
for i, j being Nat st [i,j] in Indices (1. (K,n)) holds
(1. (K,n)) * (i,j) = (RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),l,k,a)) * (i,j) by A1, A2, Lm4;
then A3: 1. (K,n) = RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),l,k,a) by MATRIX_0:27;
set b = - a;
set A = RLineXS ((1. (K,n)),l,k,a);
a + (- a) = 0. K by RLVECT_1:def 10;
then a = - (- a) by RLVECT_1:6;
then for i, j being Nat st [i,j] in Indices (1. (K,n)) holds
(1. (K,n)) * (i,j) = (RLineXS ((RLineXS ((1. (K,n)),l,k,a)),l,k,(- a))) * (i,j) by A1, A2, Lm4;
then A4: 1. (K,n) = RLineXS ((RLineXS ((1. (K,n)),l,k,a)),l,k,(- a)) by MATRIX_0:27;
( (RLineXS ((1. (K,n)),l,k,a)) * (RLineXS ((1. (K,n)),l,k,(- a))) = RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),l,k,a) & (RLineXS ((1. (K,n)),l,k,(- a))) * (RLineXS ((1. (K,n)),l,k,a)) = RLineXS ((RLineXS ((1. (K,n)),l,k,a)),l,k,(- a)) ) by A1, Th8;
then A5: RLineXS ((1. (K,n)),l,k,(- a)) is_reverse_of RLineXS ((1. (K,n)),l,k,a) by A3, A4, MATRIX_6:def 2;
then RLineXS ((1. (K,n)),l,k,a) is invertible by MATRIX_6:def 3;
hence ( RLineXS ((1. (K,n)),l,k,a) is invertible & (RLineXS ((1. (K,n)),l,k,a)) ~ = RLineXS ((1. (K,n)),l,k,(- a)) ) by A5, MATRIX_6:def 4; :: thesis: verum