defpred S₁[ Element of NAT , set , set ] means for p, q being Element of CQC-WFF st p = f . [$1,$2] & q = g . [($1 + n),$2] holds
$3 = p '&' q;
A1: for k being Element of NAT
for h being Element of Funcs (bound_QC-variables,bound_QC-variables) ex u being Element of CQC-WFF st S₁[k,h,u]

proof

let k be Element of NAT ; :: thesis: for h being Element of Funcs (bound_QC-variables,bound_QC-variables) ex u being Element of CQC-WFF st S₁[k,h,u]
let h be Element of Funcs (bound_QC-variables,bound_QC-variables); :: thesis: ex u being Element of CQC-WFF st S₁[k,h,u]
reconsider p = f . [k,h] as Element of CQC-WFF ;
reconsider q = g . [(k + n),h] as Element of CQC-WFF ;
take p '&' q ; :: thesis: S₁[k,h,p '&' q]
let p1, q1 be Element of CQC-WFF ; :: thesis: ( p1 = f . [k,h] & q1 = g . [(k + n),h] implies p '&' q = p1 '&' q1 )
assume that
A2: p1 = f . [k,h] and
A3: q1 = g . [(k + n),h] ; :: thesis: p '&' q = p1 '&' q1
thus p '&' q = p1 '&' q1 by A2, A3; :: thesis: verum

end;

consider F being Function of [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF such that
A4: for k being Element of NAT
for h being Element of Funcs (bound_QC-variables,bound_QC-variables) holds S₁[k,h,F . (k,h)] from BINOP_1:sch 3(A1);
reconsider F = F as Element of Funcs ([:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF) by FUNCT_2:11;
take F ; :: thesis: for k being Element of NAT
for h being Element of Funcs (bound_QC-variables,bound_QC-variables)
for p, q being Element of CQC-WFF st p = f . (k,h) & q = g . ((k + n),h) holds
F . (k,h) = p '&' q
let k be Element of NAT ; :: thesis: for h being Element of Funcs (bound_QC-variables,bound_QC-variables)
for p, q being Element of CQC-WFF st p = f . (k,h) & q = g . ((k + n),h) holds
F . (k,h) = p '&' q
let h be Element of Funcs (bound_QC-variables,bound_QC-variables); :: thesis: for p, q being Element of CQC-WFF st p = f . (k,h) & q = g . ((k + n),h) holds
F . (k,h) = p '&' q
let p, q be Element of CQC-WFF ; :: thesis: ( p = f . (k,h) & q = g . ((k + n),h) implies F . (k,h) = p '&' q )
assume that
A5: p = f . (k,h) and
A6: q = g . ((k + n),h) ; :: thesis: F . (k,h) = p '&' q
thus F . (k,h) = p '&' q by A4, A5, A6; :: thesis: verum