let n be Nat; :: thesis: for K being comRing
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 comRing; :: 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:87;
A6: j in Seg (width (1. (K,n))) by A1, ZFMISC_1:87;
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:87;

now :: thesis: ( ( i = l & (RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),l,k,a)) * (i,j) = (1. (K,n)) * (i,j) ) or ( i <> l & (RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),l,k,a)) * (i,j) = (1. (K,n)) * (i,j) ) )

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:28
.= ((a + (- a)) * p1) + p2 by FVSUM_1:55
.= ((0. K) * p1) + p2 by RLVECT_1:5
.= ((width (RLineXS ((1. (K,n)),l,k,(- a)))) |-> (0. K)) + p2 by FVSUM_1:58
.= Line ((1. (K,n)),i) by FVSUM_1:21 ;
hence (RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),l,k,a)) * (i,j) = (Line ((1. (K,n)),i)) . j by A6, A7, MATRIX_0:def 7
.= (1. (K,n)) * (i,j) by A6, MATRIX_0:def 7 ;
:: 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_0:def 7
.= (Line ((1. (K,n)),i)) . j by A2, A3, A5, A12, A13, Th5
.= (1. (K,n)) * (i,j) by A6, MATRIX_0:def 7 ; :: 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