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

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

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

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

end;

suppose A2: for a being Ordinal holds not a in dom f ; :: thesis: base- f = inf (dom f)

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

now :: thesis: not On (dom f) <> {}

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

end;

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

end;

end;