let A be QC-alphabet ; :: thesis:
QC-WFF A is A -closed by QC_LANG1:7;
then QC-WFF A is Subset of ([:NAT,(QC-symbols A):] *) ;
hence [:(QC-WFF A),(vSUB A):] is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] by ZFMISC_1:95; :: thesis:
thus for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):] :: thesis:

proof

let k be Nat; :: thesis:
let p be QC-pred_symbol of k,A; :: thesis:
let ll be QC-variable_list of k,A; :: thesis:
let e be Element of vSUB A; :: thesis:
p ! ll = <*p*> ^ ll by QC_LANG1:8;
hence [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):] by ZFMISC_1:def 2; :: thesis:

end;

VERUM A in QC-WFF A ;
hence for e being Element of vSUB A holds [<*[0,0]*>,e] in [:(QC-WFF A),(vSUB A):] by ZFMISC_1:def 2; :: thesis:
thus for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] holds
[(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] :: thesis:

proof

let p be FinSequence of [:NAT,(QC-symbols A):]; :: thesis:
let e be Element of vSUB A; :: thesis:
assume [p,e] in [:(QC-WFF A),(vSUB A):] ; :: thesis:
then ex a, b being object st
( a in QC-WFF A & b in vSUB A & [p,e] = [a,b] ) by ZFMISC_1:def 2;
then reconsider p9 = p as Element of QC-WFF A by XTUPLE_0:1;
'not' p9 = <*[1,0]*> ^ (@ p9) ;
hence [(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] by ZFMISC_1:def 2; :: thesis:

end;

thus for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] holds
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] :: thesis:

proof

let p, q be FinSequence of [:NAT,(QC-symbols A):]; :: thesis:
let e be Element of vSUB A; :: thesis:
assume that
A1: [p,e] in [:(QC-WFF A),(vSUB A):] and
A2: [q,e] in [:(QC-WFF A),(vSUB A):] ; :: thesis:
ex c, d being object st
( c in QC-WFF A & d in vSUB A & [q,e] = [c,d] ) by A2, ZFMISC_1:def 2;
then reconsider q9 = q as Element of QC-WFF A by XTUPLE_0:1;
ex a, b being object st
( a in QC-WFF A & b in vSUB A & [p,e] = [a,b] ) by A1, ZFMISC_1:def 2;
then reconsider p9 = p as Element of QC-WFF A by XTUPLE_0:1;
p9 '&' q9 = (<*[2,0]*> ^ (@ p9)) ^ (@ q9) ;
hence [((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] by ZFMISC_1:def 2; :: thesis:

end;

thus for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] :: thesis:

proof

let x be bound_QC-variable of A; :: thesis:
let p be FinSequence of [:NAT,(QC-symbols A):]; :: thesis:
let e be Element of vSUB A; :: thesis:
assume [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] ; :: thesis:
then ex a, b being object st
( a in QC-WFF A & b in vSUB A & [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] = [a,b] ) by ZFMISC_1:def 2;
then reconsider p9 = p as Element of QC-WFF A by XTUPLE_0:1;
All (x,p9) = (<*[3,0]*> ^ <*x*>) ^ (@ p9) ;
hence [((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] by ZFMISC_1:def 2; :: thesis:

end;