QC-WFF is Subset of ([:NAT ,NAT :] * ) by QC_LANG1:21, QC_LANG1:def 9;
hence [:QC-WFF ,vSUB :] is Subset of [:([:NAT ,NAT :] * ),vSUB :] by ZFMISC_1:118; :: thesis: ( ( for k being Element of NAT
for p being QC-pred_symbol of k
for ll being QC-variable_list of k
for e being Element of vSUB holds [(<*p*> ^ ll),e] in [:QC-WFF ,vSUB :] ) & ( for e being Element of vSUB holds [<*[0 ,0 ]*>,e] in [:QC-WFF ,vSUB :] ) & ( for p being FinSequence of [:NAT ,NAT :]
for e being Element of vSUB st [p,e] in [:QC-WFF ,vSUB :] holds
[(<*[1,0 ]*> ^ p),e] in [:QC-WFF ,vSUB :] ) & ( for p, q being FinSequence of [:NAT ,NAT :]
for e being Element of vSUB st [p,e] in [:QC-WFF ,vSUB :] & [q,e] in [:QC-WFF ,vSUB :] holds
[((<*[2,0 ]*> ^ p) ^ q),e] in [:QC-WFF ,vSUB :] ) & ( for x being bound_QC-variable
for p being FinSequence of [:NAT ,NAT :]
for e being Element of vSUB st [p,(QSub . [((<*[3,0 ]*> ^ <*x*>) ^ p),e])] in [:QC-WFF ,vSUB :] holds
[((<*[3,0 ]*> ^ <*x*>) ^ p),e] in [:QC-WFF ,vSUB :] ) )
thus for k being Element of NAT
for p being QC-pred_symbol of k
for ll being QC-variable_list of k
for e being Element of vSUB holds [(<*p*> ^ ll),e] in [:QC-WFF ,vSUB :] :: thesis: ( ( for e being Element of vSUB holds [<*[0 ,0 ]*>,e] in [:QC-WFF ,vSUB :] ) & ( for p being FinSequence of [:NAT ,NAT :]
for e being Element of vSUB st [p,e] in [:QC-WFF ,vSUB :] holds
[(<*[1,0 ]*> ^ p),e] in [:QC-WFF ,vSUB :] ) & ( for p, q being FinSequence of [:NAT ,NAT :]
for e being Element of vSUB st [p,e] in [:QC-WFF ,vSUB :] & [q,e] in [:QC-WFF ,vSUB :] holds
[((<*[2,0 ]*> ^ p) ^ q),e] in [:QC-WFF ,vSUB :] ) & ( for x being bound_QC-variable
for p being FinSequence of [:NAT ,NAT :]
for e being Element of vSUB st [p,(QSub . [((<*[3,0 ]*> ^ <*x*>) ^ p),e])] in [:QC-WFF ,vSUB :] holds
[((<*[3,0 ]*> ^ <*x*>) ^ p),e] in [:QC-WFF ,vSUB :] ) )

proof

let k be Element of NAT ; :: thesis: for p being QC-pred_symbol of k
for ll being QC-variable_list of k
for e being Element of vSUB holds [(<*p*> ^ ll),e] in [:QC-WFF ,vSUB :]
let p be QC-pred_symbol of k; :: thesis: for ll being QC-variable_list of k
for e being Element of vSUB holds [(<*p*> ^ ll),e] in [:QC-WFF ,vSUB :]
let ll be QC-variable_list of k; :: thesis: for e being Element of vSUB holds [(<*p*> ^ ll),e] in [:QC-WFF ,vSUB :]
let e be Element of vSUB ; :: thesis: [(<*p*> ^ ll),e] in [:QC-WFF ,vSUB :]
p ! ll = <*p*> ^ ll by QC_LANG1:23;
hence [(<*p*> ^ ll),e] in [:QC-WFF ,vSUB :] by ZFMISC_1:def 2; :: thesis: verum

end;

thus for e being Element of vSUB holds [<*[0 ,0 ]*>,e] in [:QC-WFF ,vSUB :] by QC_LANG1:def 13, ZFMISC_1:def 2; :: thesis: ( ( for p being FinSequence of [:NAT ,NAT :]
for e being Element of vSUB st [p,e] in [:QC-WFF ,vSUB :] holds
[(<*[1,0 ]*> ^ p),e] in [:QC-WFF ,vSUB :] ) & ( for p, q being FinSequence of [:NAT ,NAT :]
for e being Element of vSUB st [p,e] in [:QC-WFF ,vSUB :] & [q,e] in [:QC-WFF ,vSUB :] holds
[((<*[2,0 ]*> ^ p) ^ q),e] in [:QC-WFF ,vSUB :] ) & ( for x being bound_QC-variable
for p being FinSequence of [:NAT ,NAT :]
for e being Element of vSUB st [p,(QSub . [((<*[3,0 ]*> ^ <*x*>) ^ p),e])] in [:QC-WFF ,vSUB :] holds
[((<*[3,0 ]*> ^ <*x*>) ^ p),e] in [:QC-WFF ,vSUB :] ) )
thus for p being FinSequence of [:NAT ,NAT :]
for e being Element of vSUB st [p,e] in [:QC-WFF ,vSUB :] holds
[(<*[1,0 ]*> ^ p),e] in [:QC-WFF ,vSUB :] :: thesis: ( ( for p, q being FinSequence of [:NAT ,NAT :]
for e being Element of vSUB st [p,e] in [:QC-WFF ,vSUB :] & [q,e] in [:QC-WFF ,vSUB :] holds
[((<*[2,0 ]*> ^ p) ^ q),e] in [:QC-WFF ,vSUB :] ) & ( for x being bound_QC-variable
for p being FinSequence of [:NAT ,NAT :]
for e being Element of vSUB st [p,(QSub . [((<*[3,0 ]*> ^ <*x*>) ^ p),e])] in [:QC-WFF ,vSUB :] holds
[((<*[3,0 ]*> ^ <*x*>) ^ p),e] in [:QC-WFF ,vSUB :] ) )

proof

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

end;

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

proof

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

end;

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

proof

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

end;