let x be set ; :: according to FUNCT_1:def 19 :: thesis: ( not x in D ^omega or x is set )
assume x in D ^omega ; :: thesis: x is set
hence x is Function by Def8; :: thesis: verum