let l, n, k be Nat; :: thesis: 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; :: 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 A1: ( l in dom (1. K,n) & k in dom (1. K,n) & 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 A = RLineXS (1. K,n),l,k,a;
set B = RLineXS (1. K,n),l,k,(- a);
A2: ( (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;
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, Lm4;
then A3: 1. K,n = RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a by MATRIX_1:28;
set b = - a;
a + (- a) = 0. K by RLVECT_1:def 11;
then a = - (- a) by RLVECT_1:19;
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, Lm4;
then 1. K,n = RLineXS (RLineXS (1. K,n),l,k,a),l,k,(- a) by MATRIX_1:28;
then A4: RLineXS (1. K,n),l,k,(- a) is_reverse_of RLineXS (1. K,n),l,k,a by A2, A3, 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 A4, MATRIX_6:def 4; :: thesis: verum