thus f . x is Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF ; :: thesis: verum