:: deftheorem Def7 defines the_scope_of GOEDELCP:def 7 :
for Al being QC-alphabet
for F being sequence of (CQC-WFF Al)
for a being Nat
for b₄ being Element of CQC-WFF Al holds
( b₄ = the_scope_of (F,a) iff for p being Element of CQC-WFF Al st p = F . a holds
b₄ = Ex-the_scope_of p );