let f be FinSequence of (TOP-REAL 2); for i, n being Nat st i + 1 <= len (f | n) holds
LSeg ((f | n),i) = LSeg (f,i)
let i, n be Nat; ( i + 1 <= len (f | n) implies LSeg ((f | n),i) = LSeg (f,i) )
assume A1:
i + 1 <= len (f | n)
; LSeg ((f | n),i) = LSeg (f,i)
per cases
( i <> 0 or i = 0 )
;
suppose
i <> 0
;
LSeg ((f | n),i) = LSeg (f,i)then A2:
1
<= i
by NAT_1:14;
then A3:
i in dom (f | n)
by A1, SEQ_4:134;
len (f | n) <= len f
by FINSEQ_5:16;
then A4:
i + 1
<= len f
by A1, XXREAL_0:2;
A5:
i + 1
in dom (f | n)
by A1, A2, SEQ_4:134;
thus LSeg (
(f | n),
i) =
LSeg (
((f | n) /. i),
((f | n) /. (i + 1)))
by A1, A2, TOPREAL1:def 3
.=
LSeg (
(f /. i),
((f | n) /. (i + 1)))
by A3, FINSEQ_4:70
.=
LSeg (
(f /. i),
(f /. (i + 1)))
by A5, FINSEQ_4:70
.=
LSeg (
f,
i)
by A2, A4, TOPREAL1:def 3
;
verum end; end;