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