let x be Real; 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; 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; 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 ; ( 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
; ( 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}
; 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 ;
( x1 in rng (D2 | (indx (D2,D1,j1))) implies x1 in rng (D1 | j1) )
assume
x1 in rng (D2 | (indx (D2,D1,j1)))
;
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
;
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;
verum
end;
A27:
(
D2 . k in {x} implies
D2 . k = D1 . j1 )
A28:
(
D2 . k in {x} implies
D2 . k in rng (D1 | j1) )
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;
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 ;
( x1 in rng (D1 | j1) implies x1 in rng (D2 | (indx (D2,D1,j1))) )
assume
x1 in rng (D1 | j1)
;
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;
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; verum