let a be Ordinal; :: thesis: for f being Function holds
( ( f is a -based & f is segmental ) iff ex b being Ordinal st
( dom f = b \ a & a c= b ) )
let f be Function; :: thesis: ( ( f is a -based & f is segmental ) iff ex b being Ordinal st
( dom f = b \ a & a c= b ) )
thus ( f is a -based & f is segmental implies ex b being Ordinal st
( dom f = b \ a & a c= b ) ) :: thesis: ( ex b being Ordinal st
( dom f = b \ a & a c= b ) implies ( f is a -based & f is segmental ) )

proof

assume A1: for b being Ordinal st b in dom f holds
( a in dom f & a c= b ) ; :: according to EXCHSORT:def 2 :: thesis: ( not f is segmental or ex b being Ordinal st
( dom f = b \ a & a c= b ) )
given c, d being Ordinal such that A2: dom f = c \ d ; :: according to EXCHSORT:def 1 :: thesis: ex b being Ordinal st
( dom f = b \ a & a c= b )
set x = the Element of c \ d;

per cases ( dom f = {} or dom f <> {} ) ;

suppose dom f = {} ; :: thesis: ex b being Ordinal st
( dom f = b \ a & a c= b )

then a \ a = dom f by XBOOLE_1:37;
hence ex b being Ordinal st
( dom f = b \ a & a c= b ) ; :: thesis: verum

end;

suppose dom f <> {} ; :: thesis: ex b being Ordinal st
( dom f = b \ a & a c= b )

then the Element of c \ d in dom f by A2;
then a in dom f by A1;
then A3: ( d c= a & a in c ) by A2, ORDINAL6:5;
then d in c by ORDINAL1:12;
then d in dom f by A2, ORDINAL6:5;
then a c= d by A1;
then ( a = d & a c= c ) by A3, ORDINAL1:def 2;
hence ex b being Ordinal st
( dom f = b \ a & a c= b ) by A2; :: thesis: verum

end;

end;

end;

given b being Ordinal such that A4: ( dom f = b \ a & a c= b ) ; :: thesis: ( f is a -based & f is segmental )
thus f is a -based :: thesis: f is segmental

proof

let c be Ordinal; :: according to EXCHSORT:def 2 :: thesis: ( c in proj1 f implies ( a in proj1 f & a c= c ) )
assume A5: c in dom f ; :: thesis: ( a in proj1 f & a c= c )
then ( a c= c & c in b ) by A4, ORDINAL6:5;
then a in b by ORDINAL1:12;
hence ( a in proj1 f & a c= c ) by A4, A5, ORDINAL6:5; :: thesis: verum

end;

take b ; :: according to EXCHSORT:def 1 :: thesis: ex b being Ordinal st proj1 f = b \ b
take a ; :: thesis: proj1 f = b \ a
thus proj1 f = b \ a by A4; :: thesis: verum