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