defpred S_{1}[ 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 S_{1}[t,h,u]

A4: for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds S_{1}[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 ; :: thesis: 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; :: thesis: 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)); :: thesis: 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; :: thesis: ( 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) ; :: thesis: F . (t,h) = p '&' q

thus F . (t,h) = p '&' q by A4, A5, A6; :: thesis: verum

$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 S

proof

consider F being Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A) such that
let t be QC-symbol of A; :: thesis: for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) ex u being Element of CQC-WFF A st S_{1}[t,h,u]

let h be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: ex u being Element of CQC-WFF A st S_{1}[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 ; :: thesis: S_{1}[t,h,p '&' q]

let p1, q1 be Element of CQC-WFF A; :: thesis: ( 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] ; :: thesis: p '&' q = p1 '&' q1

thus p '&' q = p1 '&' q1 by A2, A3; :: thesis: verum

end;let h be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: ex u being Element of CQC-WFF A st S

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 ; :: thesis: S

let p1, q1 be Element of CQC-WFF A; :: thesis: ( 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] ; :: thesis: p '&' q = p1 '&' q1

thus p '&' q = p1 '&' q1 by A2, A3; :: thesis: verum

A4: for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds S

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 ; :: thesis: 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; :: thesis: 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)); :: thesis: 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; :: thesis: ( 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) ; :: thesis: F . (t,h) = p '&' q

thus F . (t,h) = p '&' q by A4, A5, A6; :: thesis: verum