let n be Nat; :: thesis: for K being Field
for i, j, l, k being Nat
for a being Element of K st [i,j] in Indices (1. K,n) & l in dom (1. K,n) & k in dom (1. K,n) & k <> l holds
(1. K,n) * i,j = (RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a) * i,j
let K be Field; :: thesis: for i, j, l, k being Nat
for a being Element of K st [i,j] in Indices (1. K,n) & l in dom (1. K,n) & k in dom (1. K,n) & k <> l holds
(1. K,n) * i,j = (RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a) * i,j
let i, j, l, k be Nat; :: thesis: for a being Element of K st [i,j] in Indices (1. K,n) & l in dom (1. K,n) & k in dom (1. K,n) & k <> l holds
(1. K,n) * i,j = (RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a) * i,j
let a be Element of K; :: thesis: ( [i,j] in Indices (1. K,n) & l in dom (1. K,n) & k in dom (1. K,n) & k <> l implies (1. K,n) * i,j = (RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a) * i,j )
assume A1: ( [i,j] in Indices (1. K,n) & l in dom (1. K,n) & k in dom (1. K,n) & k <> l ) ; :: thesis: (1. K,n) * i,j = (RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a) * i,j
then A2: ( i in dom (1. K,n) & j in Seg (width (1. K,n)) ) by ZFMISC_1:106;
set B = RLineXS (1. K,n),l,k,(- a);
A3: ( len (RLineXS (1. K,n),l,k,(- a)) = len (1. K,n) & width (RLineXS (1. K,n),l,k,(- a)) = width (1. K,n) ) by A1, Def3, Th1;
A4: dom (RLineXS (1. K,n),l,k,(- a)) = Seg (len (RLineXS (1. K,n),l,k,(- a))) by FINSEQ_1:def 3
.= Seg (len (1. K,n)) by A1, Def3
.= dom (1. K,n) by FINSEQ_1:def 3 ;
then A5: ( len (RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a) = len (RLineXS (1. K,n),l,k,(- a)) & width (RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a) = width (RLineXS (1. K,n),l,k,(- a)) ) by A1, Def3, Th1;
A6: i in dom (RLineXS (1. K,n),l,k,(- a)) by A1, A4, ZFMISC_1:106;

now

per cases ( i = l or i <> l ) ;

case A7: i = l ; :: thesis: (RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a) * i,j = (1. K,n) * i,j

then A8: Line (RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a),i = (a * (Line (RLineXS (1. K,n),l,k,(- a)),k)) + (Line (RLineXS (1. K,n),l,k,(- a)),i) by A1, A4, Th5;
A9: Line (RLineXS (1. K,n),l,k,(- a)),k = Line (1. K,n),k by A1, Th5;
reconsider p1 = Line (1. K,n),k as Element of (width (RLineXS (1. K,n),l,k,(- a))) -tuples_on the carrier of K by Th1;
reconsider p2 = Line (1. K,n),i as Element of (width (RLineXS (1. K,n),l,k,(- a))) -tuples_on the carrier of K by Th1;
Line (RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a),i = (a * p1) + (((- a) * p1) + p2) by A1, A7, A8, A9, Th5
.= ((a * p1) + ((- a) * p1)) + p2 by FINSEQOP:29
.= ((a + (- a)) * p1) + p2 by FVSUM_1:68
.= ((0. K) * p1) + p2 by RLVECT_1:16
.= ((width (RLineXS (1. K,n),l,k,(- a))) |-> (0. K)) + p2 by FVSUM_1:71
.= Line (1. K,n),i by FVSUM_1:28 ;
hence (RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a) * i,j = (Line (1. K,n),i) . j by A2, A3, A5, MATRIX_1:def 8
.= (1. K,n) * i,j by A2, MATRIX_1:def 8 ;
:: thesis: verum

end;

case A10: i <> l ; :: thesis: (RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a) * i,j = (1. K,n) * i,j

then A11: Line (RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a),i = Line (RLineXS (1. K,n),l,k,(- a)),i by A1, A4, A6, Th5;
thus (RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a) * i,j = (Line (RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a),i) . j by A2, A3, A5, MATRIX_1:def 8
.= (Line (1. K,n),i) . j by A1, A2, A10, A11, Th5
.= (1. K,n) * i,j by A2, MATRIX_1:def 8 ; :: thesis: verum

end;

end;

end;

hence (1. K,n) * i,j = (RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a) * i,j ; :: thesis: verum