let f be FinSequence of (TOP-REAL 2); :: thesis: for i, j being Nat st i + j = len f holds
LSeg (f,i) = LSeg ((Rev f),j)
let i, j be Nat; :: thesis: ( i + j = len f implies LSeg (f,i) = LSeg ((Rev f),j) )
assume A1: i + j = len f ; :: thesis: LSeg (f,i) = LSeg ((Rev f),j)

per cases ( ( 1 <= i & i + 1 <= len f ) or not 1 <= i or not i + 1 <= len f ) ;

suppose that A2: 1 <= i and
A3: i + 1 <= len f ; :: thesis: LSeg (f,i) = LSeg ((Rev f),j)

A4: i + (j + 1) = (len f) + 1 by A1;
A5: i in dom f by A2, A3, SEQ_4:134;
then j + 1 in dom (Rev f) by A4, FINSEQ_5:59;
then A6: j + 1 <= len (Rev f) by FINSEQ_3:25;
A7: (i + 1) + j = (len f) + 1 by A1;
A8: i + 1 in dom f by A2, A3, SEQ_4:134;
then j in dom (Rev f) by A7, FINSEQ_5:59;
then A9: 1 <= j by FINSEQ_3:25;
thus LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A2, A3, TOPREAL1:def 3
.= LSeg (((Rev f) /. (j + 1)),(f /. (i + 1))) by A5, A4, FINSEQ_5:66
.= LSeg (((Rev f) /. j),((Rev f) /. (j + 1))) by A8, A7, FINSEQ_5:66
.= LSeg ((Rev f),j) by A6, A9, TOPREAL1:def 3 ; :: thesis: verum

end;

suppose A10: not 1 <= i ; :: thesis: LSeg (f,i) = LSeg ((Rev f),j)

then i = 0 by NAT_1:14;
then not j + 1 <= len f by A1, NAT_1:13;
then A11: not j + 1 <= len (Rev f) by FINSEQ_5:def 3;
LSeg (f,i) = {} by A10, TOPREAL1:def 3;
hence LSeg (f,i) = LSeg ((Rev f),j) by A11, TOPREAL1:def 3; :: thesis: verum

end;

suppose A12: not i + 1 <= len f ; :: thesis: LSeg (f,i) = LSeg ((Rev f),j)

then A13: LSeg (f,i) = {} by TOPREAL1:def 3;
j < 1 by A1, A12, XREAL_1:6;
hence LSeg (f,i) = LSeg ((Rev f),j) by A13, TOPREAL1:def 3; :: thesis: verum

end;

end;