defpred S₁[ set , set ] means for p being Element of CQC-WFF A st p = f . $1 holds
$2 = 'not' p;
A1: for e being Element of D ex u being Element of CQC-WFF A st S₁[e,u]

proof

let e be Element of D; :: thesis: ex u being Element of CQC-WFF A st S₁[e,u]
reconsider p = f . e as Element of CQC-WFF A ;
take 'not' p ; :: thesis: S₁[e, 'not' p]
thus S₁[e, 'not' p] ; :: thesis: verum

end;

consider F being Function of D,(CQC-WFF A) such that
A2: for e being Element of D holds S₁[e,F . e] from FUNCT_2:sch 3(A1);
F is Element of Funcs (D,(CQC-WFF A)) by FUNCT_2:8;
hence ex b₁ being Element of Funcs (D,(CQC-WFF A)) st
for a being Element of D
for p being Element of CQC-WFF A st p = f . a holds
b₁ . a = 'not' p by A2; :: thesis: verum