let k, l, n be 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)) )
let K be 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)) )
let a be Element of K; ( 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
; ( 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; verum