let f be Function; :: thesis:
set A = f;
set b = inf (dom f);
A1: f is inf (dom f) -based by Th12;

suppose ex a being Ordinal st a in dom f ; :: thesis:

hence base- f = inf (dom f) by A1, Def4; :: thesis:

end;

suppose A2: for a being Ordinal holds not a in dom f ; :: thesis:

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

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

end;

then inf (dom f) = 0 by SETFAM_1:def 1;
hence base- f = inf (dom f) by A2, Def4; :: thesis:

end;

end;