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)

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 )
;

end;

suppose that A2:
1 <= i
and

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

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;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

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;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