let b be Ordinal; for f being Function holds
( ( f is b -limited & not f is empty & f is segmental ) iff ex a being Ordinal 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 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 st
( dom f = b \ a & a in b ) )
( ex a being Ordinal 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 st
( dom f = b \ a & a in b ) )
assume A2:
not
f is
empty
;
( not f is segmental or ex a being Ordinal st
( dom f = b \ a & a in b ) )
given c,
d being
Ordinal such that A3:
dom f = c \ d
;
EXCHSORT:def 1 ex a being Ordinal 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 )
A4:
b = c
by A2, A1, A3, Th6;
thus
dom f = b \ a
by A2, A1, A3, Th6;
a in b
(
a c= the
Element of
c \ d & the
Element of
c \ d in b )
by A2, A3, A4, ORDINAL6:5;
hence
a in b
by ORDINAL1:12;
verum
end;
given a being Ordinal such that A5:
( dom f = b \ a & a in b )
; ( f is b -limited & not f is empty & f is segmental )
a in dom f
by A5, ORDINAL6:5;
hence
b = sup (dom f)
by A5, Th6; EXCHSORT:def 3 ( not f is empty & f is segmental )
thus
not f is empty
by A5, ORDINAL6:5; f is segmental
take
b
; EXCHSORT:def 1 ex b being Ordinal st proj1 f = b \ b
take
a
; proj1 f = b \ a
thus
proj1 f = b \ a
by A5; verum