let f be Function; :: thesis: base- f = inf (dom f)
set A = f;
set b = inf (dom f);
A0: f is inf (dom f) -based by Th003;

per cases ( ex a being ordinal number st a in dom f or for a being ordinal number holds not a in dom f ) ;

suppose ex a being ordinal number st a in dom f ; :: thesis: base- f = inf (dom f)

hence base- f = inf (dom f) by A0, BA; :: thesis: verum

end;

suppose A1: for a being ordinal number holds not a in dom f ; :: thesis: base- f = inf (dom f)

set x = the Element of On (dom f);

now

assume On (dom f) <> {} ; :: thesis: contradiction
then the Element of On (dom f) in dom f by ORDINAL1:def 9;
hence contradiction by A1; :: thesis: verum

end;

then inf (dom f) = 0 by SETFAM_1:def 1;
hence base- f = inf (dom f) by A1, BA; :: thesis: verum

end;

end;