let a be ordinal number ; :: thesis: for f being Function holds
( ( f is a -based & f is segmental ) iff ex b being ordinal number 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 number st
( dom f = b \ a & a c= b ) )
thus ( f is a -based & f is segmental implies ex b being ordinal number st
( dom f = b \ a & a c= b ) ) :: thesis: ( ex b being ordinal number st
( dom f = b \ a & a c= b ) implies ( f is a -based & f is segmental ) )

proof

assume A1: for b being ordinal number 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 number st
( dom f = b \ a & a c= b ) )
given c, d being ordinal number such that A2: dom f = c \ d ; :: according to EXCHSORT:def 1 :: thesis: ex b being ordinal number 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 number st
( dom f = b \ a & a c= b )

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

end;

suppose dom f <> {} ; :: thesis: ex b being ordinal number 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 A4: ( 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 A4, ORDINAL1:def 2, XBOOLE_0:def 10;
hence ex b being ordinal number st
( dom f = b \ a & a c= b ) by A2; :: thesis: verum

end;

end;

end;

given b being ordinal number such that B1: ( 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 number ; :: according to EXCHSORT:def 2 :: thesis: ( c in proj1 f implies ( a in proj1 f & a c= c ) )
assume B2: c in dom f ; :: thesis: ( a in proj1 f & a c= c )
then ( a c= c & c in b ) by B1, ORDINAL6:5;
then a in b by ORDINAL1:12;
hence ( a in proj1 f & a c= c ) by B1, B2, ORDINAL6:5; :: thesis: verum

end;

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