let x be Real; :: thesis: for A being non empty closed_interval Subset of REAL
for D1, D2 being Division of A
for j1 being Element of NAT st j1 = (len D1) - 1 & x in divset (D1,(len D1)) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} holds
rng (D2 | (indx (D2,D1,j1))) = rng (D1 | j1)

let A be non empty closed_interval Subset of REAL; :: thesis: for D1, D2 being Division of A
for j1 being Element of NAT st j1 = (len D1) - 1 & x in divset (D1,(len D1)) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} holds
rng (D2 | (indx (D2,D1,j1))) = rng (D1 | j1)

let D1, D2 be Division of A; :: thesis: for j1 being Element of NAT st j1 = (len D1) - 1 & x in divset (D1,(len D1)) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} holds
rng (D2 | (indx (D2,D1,j1))) = rng (D1 | j1)

let j1 be Element of NAT ; :: thesis: ( j1 = (len D1) - 1 & x in divset (D1,(len D1)) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} implies rng (D2 | (indx (D2,D1,j1))) = rng (D1 | j1) )
assume that
A1: j1 = (len D1) - 1 and
A2: x in divset (D1,(len D1)) and
A3: len D1 >= 2 ; :: thesis: ( not D1 <= D2 or not rng D2 = (rng D1) \/ {x} or rng (D2 | (indx (D2,D1,j1))) = rng (D1 | j1) )
A4: len D1 in dom D1 by FINSEQ_5:6;
assume that
A5: D1 <= D2 and
A6: rng D2 = (rng D1) \/ {x} ; :: thesis: rng (D2 | (indx (D2,D1,j1))) = rng (D1 | j1)
A7: len D1 <> 1 by A3;
then A8: (len D1) - 1 in dom D1 by ;
then A9: indx (D2,D1,j1) in dom D2 by ;
then A10: indx (D2,D1,j1) <= len D2 by FINSEQ_3:25;
A11: j1 in dom D1 by ;
then A12: 1 <= j1 by FINSEQ_3:25;
A13: j1 <= len D1 by ;
lower_bound (divset (D1,(len D1))) <= x by ;
then A14: D1 . j1 <= x by ;
for x1 being object st x1 in rng (D2 | (indx (D2,D1,j1))) holds
x1 in rng (D1 | j1)
proof
let x1 be object ; :: thesis: ( x1 in rng (D2 | (indx (D2,D1,j1))) implies x1 in rng (D1 | j1) )
assume x1 in rng (D2 | (indx (D2,D1,j1))) ; :: thesis: x1 in rng (D1 | j1)
then consider k being Element of NAT such that
A15: k in dom (D2 | (indx (D2,D1,j1))) and
A16: x1 = (D2 | (indx (D2,D1,j1))) . k by PARTFUN1:3;
k in Seg (len (D2 | (indx (D2,D1,j1)))) by ;
then A17: k in Seg (indx (D2,D1,j1)) by ;
then A18: k in dom D2 by ;
A19: len (D1 | j1) = j1 by ;
k <= indx (D2,D1,j1) by ;
then D2 . k <= D2 . (indx (D2,D1,j1)) by ;
then A20: D2 . k <= D1 . j1 by ;
A21: ( D2 . k in rng D1 implies D2 . k in rng (D1 | j1) )
proof
assume D2 . k in rng D1 ; :: thesis: D2 . k in rng (D1 | j1)
then consider m being Element of NAT such that
A22: m in dom D1 and
A23: D2 . k = D1 . m by PARTFUN1:3;
m in Seg (len D1) by ;
then A24: 1 <= m by FINSEQ_1:1;
A25: m <= j1 by ;
then m in Seg j1 by ;
then A26: D2 . k = (D1 | j1) . m by ;
m in dom (D1 | j1) by ;
hence D2 . k in rng (D1 | j1) by ; :: thesis: verum
end;
A27: ( D2 . k in {x} implies D2 . k = D1 . j1 )
proof
assume D2 . k in {x} ; :: thesis: D2 . k = D1 . j1
then D1 . j1 <= D2 . k by ;
hence D2 . k = D1 . j1 by ; :: thesis: verum
end;
A28: ( D2 . k in {x} implies D2 . k in rng (D1 | j1) )
proof
j1 in dom (D1 | j1) by ;
then A29: (D1 | j1) . j1 in rng (D1 | j1) by FUNCT_1:def 3;
assume A30: D2 . k in {x} ; :: thesis: D2 . k in rng (D1 | j1)
j1 in Seg j1 by ;
hence D2 . k in rng (D1 | j1) by ; :: thesis: verum
end;
D2 . k in rng D2 by ;
hence x1 in rng (D1 | j1) by ; :: thesis: verum
end;
then A31: rng (D2 | (indx (D2,D1,j1))) c= rng (D1 | j1) ;
for x1 being object st x1 in rng (D1 | j1) holds
x1 in rng (D2 | (indx (D2,D1,j1)))
proof
let x1 be object ; :: thesis: ( x1 in rng (D1 | j1) implies x1 in rng (D2 | (indx (D2,D1,j1))) )
assume x1 in rng (D1 | j1) ; :: thesis: x1 in rng (D2 | (indx (D2,D1,j1)))
then consider k being Element of NAT such that
A32: k in dom (D1 | j1) and
A33: x1 = (D1 | j1) . k by PARTFUN1:3;
k in Seg (len (D1 | j1)) by ;
then A34: k in Seg j1 by ;
then A35: k in dom D1 by ;
k <= j1 by ;
then D1 . k <= D1 . j1 by ;
then D2 . (indx (D2,D1,k)) <= D1 . j1 by ;
then A36: D2 . (indx (D2,D1,k)) <= D2 . (indx (D2,D1,j1)) by ;
A37: (D1 | j1) . k = D1 . k by ;
D1 . k in rng D1 by ;
then x1 in rng D2 by ;
then consider n being Element of NAT such that
A38: n in dom D2 and
A39: x1 = D2 . n by PARTFUN1:3;
D2 . (indx (D2,D1,k)) = D2 . n by ;
then A40: n <= indx (D2,D1,j1) by ;
1 <= n by ;
then A41: n in Seg (indx (D2,D1,j1)) by ;
then n in Seg (len (D2 | (indx (D2,D1,j1)))) by ;
then A42: n in dom (D2 | (indx (D2,D1,j1))) by FINSEQ_1:def 3;
D2 . n = (D2 | (indx (D2,D1,j1))) . n by ;
hence x1 in rng (D2 | (indx (D2,D1,j1))) by ; :: thesis: verum
end;
then rng (D1 | j1) c= rng (D2 | (indx (D2,D1,j1))) ;
hence rng (D2 | (indx (D2,D1,j1))) = rng (D1 | j1) by ; :: thesis: verum