let i be Element of NAT ; :: thesis: for A being non empty closed_interval Subset of REAL
for D1, D2 being Division of A st i in dom D1 & D1 <= D2 holds
ex j being Element of NAT st
( j in dom D2 & D1 . i = D2 . j )
let A be non empty closed_interval Subset of REAL; :: thesis: for D1, D2 being Division of A st i in dom D1 & D1 <= D2 holds
ex j being Element of NAT st
( j in dom D2 & D1 . i = D2 . j )
let D1, D2 be Division of A; :: thesis: ( i in dom D1 & D1 <= D2 implies ex j being Element of NAT st
( j in dom D2 & D1 . i = D2 . j ) )
assume i in dom D1 ; :: thesis: ( not D1 <= D2 or ex j being Element of NAT st
( j in dom D2 & D1 . i = D2 . j ) )
then A1: D1 . i in rng D1 by FUNCT_1:def 3;
assume D1 <= D2 ; :: thesis: ex j being Element of NAT st
( j in dom D2 & D1 . i = D2 . j )
then rng D1 c= rng D2 ;
then consider x1 being object such that
A2: x1 in dom D2 and
A3: D1 . i = D2 . x1 by A1, FUNCT_1:def 3;
reconsider x1 = x1 as Element of NAT by A2;
take x1 ; :: thesis: ( x1 in dom D2 & D1 . i = D2 . x1 )
thus ( x1 in dom D2 & D1 . i = D2 . x1 ) by A2, A3; :: thesis: verum