let f be Function; :: thesis: f is inf (dom f) -based
set b = inf (dom f);
let c be ordinal number ; :: according to EXCHSORT:def 2 :: thesis: ( c in proj1 f implies ( inf (dom f) in proj1 f & inf (dom f) c= c ) )
assume c in dom f ; :: thesis: ( inf (dom f) in proj1 f & inf (dom f) c= c )
hence ( inf (dom f) in dom f & inf (dom f) c= c ) by ORDINAL2:14, ORDINAL2:17; :: thesis: verum