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 A4, INTEGRA1:7;
then A9: indx (D2,D1,j1) in dom D2 by A1, A5, INTEGRA1:def 19;
then A10: indx (D2,D1,j1) <= len D2 by FINSEQ_3:25;
A11: j1 in dom D1 by A1, A4, A7, INTEGRA1:7;
then A12: 1 <= j1 by FINSEQ_3:25;
A13: j1 <= len D1 by A11, FINSEQ_3:25;
lower_bound (divset (D1,(len D1))) <= x by A2, INTEGRA2:1;
then A14: D1 . j1 <= x by A1, A4, A7, INTEGRA1:def 4;
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 A15, FINSEQ_1:def 3;
then A17: k in Seg (indx (D2,D1,j1)) by A10, FINSEQ_1:59;
then A18: k in dom D2 by A9, RFINSEQ:6;
A19: len (D1 | j1) = j1 by A13, FINSEQ_1:59;
k <= indx (D2,D1,j1) by A17, FINSEQ_1:1;
then D2 . k <= D2 . (indx (D2,D1,j1)) by A9, A18, SEQ_4:137;
then A20: D2 . k <= D1 . j1 by A1, A5, A8, INTEGRA1:def 19;
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 A22, FINSEQ_1:def 3;
then A24: 1 <= m by FINSEQ_1:1;
A25: m <= j1 by A11, A20, A22, A23, SEQM_3:def 1;
then m in Seg j1 by A24, FINSEQ_1:1;
then A26: D2 . k = (D1 | j1) . m by A11, A23, RFINSEQ:6;
m in dom (D1 | j1) by A19, A24, A25, FINSEQ_3:25;
hence D2 . k in rng (D1 | j1) by A26, FUNCT_1:def 3; :: 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 A14, TARSKI:def 1;
hence D2 . k = D1 . j1 by A20, XXREAL_0:1; :: thesis: verum

end;

A28: ( D2 . k in {x} implies D2 . k in rng (D1 | j1) )

proof

j1 in dom (D1 | j1) by A12, A19, FINSEQ_3:25;
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 A12, FINSEQ_1:1;
hence D2 . k in rng (D1 | j1) by A11, A27, A30, A29, RFINSEQ:6; :: thesis: verum

end;

D2 . k in rng D2 by A18, FUNCT_1:def 3;
hence x1 in rng (D1 | j1) by A6, A9, A16, A17, A28, A21, RFINSEQ:6, XBOOLE_0:def 3; :: 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 A32, FINSEQ_1:def 3;
then A34: k in Seg j1 by A13, FINSEQ_1:59;
then A35: k in dom D1 by A11, RFINSEQ:6;
k <= j1 by A34, FINSEQ_1:1;
then D1 . k <= D1 . j1 by A1, A8, A35, SEQ_4:137;
then D2 . (indx (D2,D1,k)) <= D1 . j1 by A5, A35, INTEGRA1:def 19;
then A36: D2 . (indx (D2,D1,k)) <= D2 . (indx (D2,D1,j1)) by A1, A5, A8, INTEGRA1:def 19;
A37: (D1 | j1) . k = D1 . k by A11, A34, RFINSEQ:6;
D1 . k in rng D1 by A35, FUNCT_1:def 3;
then x1 in rng D2 by A6, A33, A37, XBOOLE_0:def 3;
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 A5, A33, A37, A35, A39, INTEGRA1:def 19;
then A40: n <= indx (D2,D1,j1) by A9, A38, A36, SEQM_3:def 1;
1 <= n by A38, FINSEQ_3:25;
then A41: n in Seg (indx (D2,D1,j1)) by A40, FINSEQ_1:1;
then n in Seg (len (D2 | (indx (D2,D1,j1)))) by A10, FINSEQ_1:59;
then A42: n in dom (D2 | (indx (D2,D1,j1))) by FINSEQ_1:def 3;
D2 . n = (D2 | (indx (D2,D1,j1))) . n by A9, A41, RFINSEQ:6;
hence x1 in rng (D2 | (indx (D2,D1,j1))) by A39, A42, FUNCT_1:def 3; :: 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 A31, XBOOLE_0:def 10; :: thesis: verum