let f be FinSequenceSet of D; :: thesis: f is functional
let x be set ; :: according to FUNCT_1:def 13 :: thesis: ( not x in f or x is set )
thus ( not x in f or x is set ) by Def3; :: thesis: verum