( a in dom f or not a in dom f ) ;
hence f . a is ordinal by Th34, FUNCT_1:def 4; :: thesis: verum