let x be bound_QC-variable; :: thesis: for S being Element of CQC-Sub-WFF st x in dom (@ (S `2 )) holds
(@ (S `2 )) . x is bound_QC-variable
let S be Element of CQC-Sub-WFF ; :: thesis: ( x in dom (@ (S `2 )) implies (@ (S `2 )) . x is bound_QC-variable )
assume x in dom (@ (S `2 )) ; :: thesis: (@ (S `2 )) . x is bound_QC-variable
then (@ (S `2 )) . x in rng (@ (S `2 )) by FUNCT_1:12;
hence (@ (S `2 )) . x is bound_QC-variable ; :: thesis: verum