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 (,) ex u being Element of CQC-WFF A st S1[t,h,u]
proof
let t be QC-symbol of A; :: thesis: for h being Element of Funcs (,) ex u being Element of CQC-WFF A st S1[t,h,u]
let h be Element of Funcs (,); :: thesis: 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 ; :: thesis: S1[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;
consider F being Function of [:(),(Funcs (,)):],() such that
A4: for t being QC-symbol of A
for h being Element of Funcs (,) holds S1[t,h,F . (t,h)] from reconsider F = F as Element of Funcs ([:(),(Funcs (,)):],()) by FUNCT_2:8;
take F ; :: thesis: for t being QC-symbol of A
for h being Element of Funcs (,)
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 (,)
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 (,); :: 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