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 A3: 1 <= i and
A4: i + 1 <= len f ; :: thesis: LSeg f,i = LSeg (Rev f),j

A5: i in dom f by A3, A4, GOBOARD2:3;
A6: i + 1 in dom f by A3, A4, GOBOARD2:3;
A7: i + (j + 1) = (len f) + 1 by A1;
then j + 1 in dom (Rev f) by A5, FINSEQ_5:62;
then A8: j + 1 <= len (Rev f) by FINSEQ_3:27;
A9: (i + 1) + j = (len f) + 1 by A1;
then j in dom (Rev f) by A6, FINSEQ_5:62;
then A10: 1 <= j by FINSEQ_3:27;
thus LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A3, A4, TOPREAL1:def 5
.= LSeg ((Rev f) /. (j + 1)),(f /. (i + 1)) by A5, A7, FINSEQ_5:69
.= LSeg ((Rev f) /. j),((Rev f) /. (j + 1)) by A6, A9, FINSEQ_5:69
.= LSeg (Rev f),j by A8, A10, TOPREAL1:def 5 ; :: thesis: verum

end;

suppose A11: 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 not j + 1 <= len (Rev f) by FINSEQ_5:def 3;
then ( LSeg f,i = {} & LSeg (Rev f),j = {} ) by A11, TOPREAL1:def 5;
hence LSeg f,i = LSeg (Rev f),j ; :: thesis: verum

end;

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

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

end;

end;