let x be object ; :: according to VALUED_0:def 12 :: thesis: ( not x in dom |.f.| or |.f.| . x is natural )
|.(f . x).| is natural ;
hence ( not x in dom |.f.| or |.f.| . x is natural ) by Def11; :: thesis: verum