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 A1: x in D ^omega ; :: thesis: x is set
thus x is set by A1, AFINSQ_1:def 8; :: thesis: verum