let D be set ; :: thesis: D ^omega is functional
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 set ; :: thesis: verum