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 that
A1: [i,j] in Indices (1. K,n) and
A2: l in dom (1. K,n) and
A3: k in dom (1. K,n) and
A4: k <> l ; :: thesis: (1. K,n) * i,j = (RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a) * i,j
A5: i in dom (1. K,n) by A1, ZFMISC_1:106;
A6: j in Seg (width (1. K,n)) by A1, ZFMISC_1:106;
set B = RLineXS (1. K,n),l,k,(- a);
A7: ( width (RLineXS (1. K,n),l,k,(- a)) = width (1. K,n) & width (RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a) = width (RLineXS (1. K,n),l,k,(- a)) ) by Th1;
A8: 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 A3, Def3
.= dom (1. K,n) by FINSEQ_1:def 3 ;
then A9: i in dom (RLineXS (1. K,n),l,k,(- a)) by A1, ZFMISC_1:106;

now

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

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

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;
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;
A11: Line (RLineXS (1. K,n),l,k,(- a)),k = Line (1. K,n),k by A2, A3, A4, Th5;
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 A2, A3, A8, A10, Th5;
then Line (RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a),i = (a * p1) + (((- a) * p1) + p2) by A2, A3, A10, A11, 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 A6, A7, MATRIX_1:def 8
.= (1. K,n) * i,j by A6, MATRIX_1:def 8 ;
:: thesis: verum

end;

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

then A13: Line (RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a),i = Line (RLineXS (1. K,n),l,k,(- a)),i by A2, A3, A8, A9, 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 A6, A7, MATRIX_1:def 8
.= (Line (1. K,n),i) . j by A2, A3, A5, A12, A13, Th5
.= (1. K,n) * i,j by A6, 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