let b be ordinal number ; for f being Function holds
( ( f is b -limited & not f is empty & f is segmental ) iff ex a being ordinal number st
( dom f = b \ a & a in b ) )
let f be Function; ( ( f is b -limited & not f is empty & f is segmental ) iff ex a being ordinal number st
( dom f = b \ a & a in b ) )
thus
( f is b -limited & not f is empty & f is segmental implies ex a being ordinal number st
( dom f = b \ a & a in b ) )
( ex a being ordinal number st
( dom f = b \ a & a in b ) implies ( f is b -limited & not f is empty & f is segmental ) )proof
assume A1:
b = sup (dom f)
;
EXCHSORT:def 3 ( f is empty or not f is segmental or ex a being ordinal number st
( dom f = b \ a & a in b ) )
assume Z0:
not
f is
empty
;
( not f is segmental or ex a being ordinal number st
( dom f = b \ a & a in b ) )
given c,
d being
ordinal number such that A2:
dom f = c \ d
;
EXCHSORT:def 1 ex a being ordinal number st
( dom f = b \ a & a in b )
set x = the
Element of
c \ d;
take a =
d;
( dom f = b \ a & a in b )
A3:
b = c
by Z0, A1, A2, Th008;
thus
dom f = b \ a
by Z0, A1, A2, Th008;
a in b
(
a c= the
Element of
c \ d & the
Element of
c \ d in b )
by Z0, A2, A3, ORDINAL6:5;
hence
a in b
by ORDINAL1:12;
verum
end;
given a being ordinal number such that Z1:
( dom f = b \ a & a in b )
; ( f is b -limited & not f is empty & f is segmental )
a in dom f
by Z1, ORDINAL6:5;
hence
b = sup (dom f)
by Z1, Th008; EXCHSORT:def 3 ( not f is empty & f is segmental )
thus
not f is empty
by Z1, ORDINAL6:5; f is segmental
take
b
; EXCHSORT:def 1 ex b being ordinal number st proj1 f = b \ b
take
a
; proj1 f = b \ a
thus
proj1 f = b \ a
by Z1; verum