let i be Element of NAT ; :: thesis: for A being non empty closed_interval Subset of REAL
for D being Division of A st i in dom D & i <> 1 holds
( i - 1 in dom D & D . (i - 1) in A & i - 1 in NAT )
let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A st i in dom D & i <> 1 holds
( i - 1 in dom D & D . (i - 1) in A & i - 1 in NAT )
let D be Division of A; :: thesis: ( i in dom D & i <> 1 implies ( i - 1 in dom D & D . (i - 1) in A & i - 1 in NAT ) )
assume that
A1: i in dom D and
A2: i <> 1 ; :: thesis: ( i - 1 in dom D & D . (i - 1) in A & i - 1 in NAT )
consider j being Nat such that
A3: dom D = Seg j by FINSEQ_1:def 2;
i <> 0 by A1, A3, FINSEQ_1:1;
then A4: not i is trivial by A2, NAT_2:def 1;
then consider l being Nat such that
A5: i = 2 + l by NAT_1:10, NAT_2:29;
reconsider l = l as Element of NAT by ORDINAL1:def 12;
i >= 2 by A4, NAT_2:29;
then A6: (1 + 1) - 1 <= i - 1 by XREAL_1:9;
i <= j by A1, A3, FINSEQ_1:1;
then A7: i - 1 <= j - 0 by XREAL_1:13;
A8: rng D c= A by Def1;
A9: l + 1 = i - (2 - 1) by A5;
then i - 1 in dom D by A3, A6, A7, FINSEQ_1:1;
then D . (i - 1) in rng D by FUNCT_1:def 3;
hence ( i - 1 in dom D & D . (i - 1) in A & i - 1 in NAT ) by A3, A6, A7, A9, A8, FINSEQ_1:1; :: thesis: verum