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