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)

for x1 being object st x1 in rng (D1 | j1) holds

x1 in rng (D2 | (indx (D2,D1,j1)))

hence rng (D2 | (indx (D2,D1,j1))) = rng (D1 | j1) by A31, XBOOLE_0:def 10; :: thesis: verum

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

then A31:
rng (D2 | (indx (D2,D1,j1))) c= rng (D1 | j1)
;
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) )

hence x1 in rng (D1 | j1) by A6, A9, A16, A17, A28, A21, RFINSEQ:6, XBOOLE_0:def 3; :: thesis: verum

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

A27:
( D2 . k in {x} implies D2 . k = D1 . j1 )
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;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

proof

A28:
( D2 . k in {x} implies D2 . k in rng (D1 | j1) )
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;then D1 . j1 <= D2 . k by A14, TARSKI:def 1;

hence D2 . k = D1 . j1 by A20, XXREAL_0:1; :: thesis: verum

proof

D2 . k in rng D2
by A18, FUNCT_1:def 3;
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;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

hence x1 in rng (D1 | j1) by A6, A9, A16, A17, A28, A21, RFINSEQ:6, XBOOLE_0:def 3; :: thesis: verum

for x1 being object st x1 in rng (D1 | j1) holds

x1 in rng (D2 | (indx (D2,D1,j1)))

proof

then
rng (D1 | j1) c= rng (D2 | (indx (D2,D1,j1)))
;
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;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

hence rng (D2 | (indx (D2,D1,j1))) = rng (D1 | j1) by A31, XBOOLE_0:def 10; :: thesis: verum