let i be Element of NAT ; :: thesis: for A being 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 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 A1: i in dom D1 ; :: thesis: ( not D1 <= D2 or ex j being Element of NAT st
( j in dom D2 & D1 . i = D2 . j ) )
assume A2: D1 <= D2 ; :: thesis: ex j being Element of NAT st
( j in dom D2 & D1 . i = D2 . j )
A3: D1 . i in rng D1 by A1, FUNCT_1:def 5;
rng D1 c= rng D2 by A2, Def20;
then consider x1 being set such that
A4: ( x1 in dom D2 & D1 . i = D2 . x1 ) by A3, FUNCT_1:def 5;
reconsider x1 = x1 as Element of NAT by A4;
take x1 ; :: thesis: ( x1 in dom D2 & D1 . i = D2 . x1 )
thus ( x1 in dom D2 & D1 . i = D2 . x1 ) by A4; :: thesis: verum