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