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, GOBOARD2:3;
then j + 1 in dom (Rev f) by A4, FINSEQ_5:62;
then A6: j + 1 <= len (Rev f) by FINSEQ_3:27;
A7: (i + 1) + j = (len f) + 1 by A1;
A8: i + 1 in dom f by A2, A3, GOBOARD2:3;
then j in dom (Rev f) by A7, FINSEQ_5:62;
then A9: 1 <= j by FINSEQ_3:27;
thus LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A2, A3, TOPREAL1:def 5
.= LSeg ((Rev f) /. (j + 1)),(f /. (i + 1)) by A5, A4, FINSEQ_5:69
.= LSeg ((Rev f) /. j),((Rev f) /. (j + 1)) by A8, A7, FINSEQ_5:69
.= LSeg (Rev f),j by A6, A9, TOPREAL1:def 5 ; :: 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 5;
hence LSeg f,i = LSeg (Rev f),j by A11, TOPREAL1:def 5; :: 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 5;
j < 1 by A1, A12, XREAL_1:8;
hence LSeg f,i = LSeg (Rev f),j by A13, TOPREAL1:def 5; :: thesis: verum

end;

end;