defpred S1[ Element of QC-symbols A, set , set ] means for p, q being Element of CQC-WFF A st p = f . [$1,$2] & q = g . [($1 + n),$2] holds
$3 = p '&' q;
A1:
for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) ex u being Element of CQC-WFF A st S1[t,h,u]
proof
let t be
QC-symbol of
A;
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) ex u being Element of CQC-WFF A st S1[t,h,u]let h be
Element of
Funcs (
(bound_QC-variables A),
(bound_QC-variables A));
ex u being Element of CQC-WFF A st S1[t,h,u]
reconsider p =
f . [t,h] as
Element of
CQC-WFF A ;
reconsider q =
g . [(t + n),h] as
Element of
CQC-WFF A ;
take
p '&' q
;
S1[t,h,p '&' q]
let p1,
q1 be
Element of
CQC-WFF A;
( p1 = f . [t,h] & q1 = g . [(t + n),h] implies p '&' q = p1 '&' q1 )
assume that A2:
p1 = f . [t,h]
and A3:
q1 = g . [(t + n),h]
;
p '&' q = p1 '&' q1
thus
p '&' q = p1 '&' q1
by A2, A3;
verum
end;
consider F being Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A) such that
A4:
for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds S1[t,h,F . (t,h)]
from BINOP_1:sch 3(A1);
reconsider F = F as Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) by FUNCT_2:8;
take
F
; for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
for p, q being Element of CQC-WFF A st p = f . (t,h) & q = g . ((t + n),h) holds
F . (t,h) = p '&' q
let t be QC-symbol of A; for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
for p, q being Element of CQC-WFF A st p = f . (t,h) & q = g . ((t + n),h) holds
F . (t,h) = p '&' q
let h be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); for p, q being Element of CQC-WFF A st p = f . (t,h) & q = g . ((t + n),h) holds
F . (t,h) = p '&' q
let p, q be Element of CQC-WFF A; ( p = f . (t,h) & q = g . ((t + n),h) implies F . (t,h) = p '&' q )
assume that
A5:
p = f . (t,h)
and
A6:
q = g . ((t + n),h)
; F . (t,h) = p '&' q
thus
F . (t,h) = p '&' q
by A4, A5, A6; verum