let F be sequence of (bool NAT); :: thesis: ( ( for x being Element of NAT holds F . x = { y where y is Element of NAT : x <= y } ) implies # (Tails OrderedNAT) = rng F )
assume A1: for x being Element of NAT holds F . x = { y where y is Element of NAT : x <= y } ; :: thesis: # (Tails OrderedNAT) = rng F
set F1 = rng F;
set F2 = { (uparrow p) where p is Element of OrderedNAT : verum } ;
now :: thesis: ( ( for t being object st t in rng F holds
t in { (uparrow p) where p is Element of OrderedNAT : verum } ) & ( for t being object st t in { (uparrow p) where p is Element of OrderedNAT : verum } holds
t in rng F ) )
hereby :: thesis: for t being object st t in { (uparrow p) where p is Element of OrderedNAT : verum } holds
t in rng F
let t be object ; :: thesis: ( t in rng F implies t in { (uparrow p) where p is Element of OrderedNAT : verum } )
assume t in rng F ; :: thesis: t in { (uparrow p) where p is Element of OrderedNAT : verum }
then consider x0 being object such that
A2: ( x0 in dom F & t = F . x0 ) by FUNCT_1:def 3;
reconsider x1 = x0 as Element of NAT by A2;
reconsider x2 = x0 as Element of OrderedNAT by A2;
t = { y where y is Element of NAT : x1 <= y } by A1, A2;
then t = { x where x is Element of OrderedNAT : x2 <= x } by Lm3;
then t = { x where x is Element of NAT : ex p0 being Element of NAT st
( x2 = p0 & p0 <= x ) } by Lm4;
then t = uparrow x2 by Th23;
hence t in { (uparrow p) where p is Element of OrderedNAT : verum } ; :: thesis: verum
end;
let t be object ; :: thesis: ( t in { (uparrow p) where p is Element of OrderedNAT : verum } implies t in rng F )
assume t in { (uparrow p) where p is Element of OrderedNAT : verum } ; :: thesis: t in rng F
then consider p0 being Element of OrderedNAT such that
A3: t = uparrow p0 ;
t = { x where x is Element of NAT : ex p1 being Element of NAT st
( p0 = p1 & p1 <= x ) } by A3, Th23;
then A4: t = { y where y is Element of OrderedNAT : p0 <= y } by Lm4;
reconsider p2 = p0 as Element of NAT ;
t = { x where x is Element of NAT : p2 <= x } by A4, Lm3;
then A5: t = F . p2 by A1;
dom F = NAT by FUNCT_2:def 1;
hence t in rng F by A5, FUNCT_1:3; :: thesis: verum
end;
then ( rng F c= { (uparrow p) where p is Element of OrderedNAT : verum } & { (uparrow p) where p is Element of OrderedNAT : verum } c= rng F ) ;
hence # (Tails OrderedNAT) = rng F ; :: thesis: verum