[:QC-WFF ,vSUB :] c= [:([:NAT ,NAT :] * ),vSUB :]
hence
[:QC-WFF ,vSUB :] is Subset of [:([:NAT ,NAT :] * ),vSUB :]
; :: thesis: ( ( for k being Element of NAT
for p being QC-pred_symbol of k
for ll being QC-variable_list of
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
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
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
for e being Element of vSUB holds [(<*p*> ^ ll),e] in [:QC-WFF ,vSUB :]let ll be
QC-variable_list of ;
:: 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 consider a,
b being
set such that A1:
(
a in QC-WFF &
b in vSUB &
[p,e] = [a,b] )
by ZFMISC_1:def 2;
reconsider p' =
p as
Element of
QC-WFF by A1, ZFMISC_1:33;
'not' p' = <*[1,0 ]*> ^ (@ p')
;
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 A2:
(
[p,e] in [:QC-WFF ,vSUB :] &
[q,e] in [:QC-WFF ,vSUB :] )
;
:: thesis: [((<*[2,0 ]*> ^ p) ^ q),e] in [:QC-WFF ,vSUB :]
then consider a,
b being
set such that A3:
(
a in QC-WFF &
b in vSUB &
[p,e] = [a,b] )
by ZFMISC_1:def 2;
reconsider p' =
p as
Element of
QC-WFF by A3, ZFMISC_1:33;
consider c,
d being
set such that A4:
(
c in QC-WFF &
d in vSUB &
[q,e] = [c,d] )
by A2, ZFMISC_1:def 2;
reconsider q' =
q as
Element of
QC-WFF by A4, ZFMISC_1:33;
p' '&' q' = (<*[2,0 ]*> ^ (@ p')) ^ (@ q')
;
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: verumproof
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 consider a,
b being
set such that A5:
(
a in QC-WFF &
b in vSUB &
[p,(QSub . [((<*[3,0 ]*> ^ <*x*>) ^ p),e])] = [a,b] )
by ZFMISC_1:def 2;
reconsider p' =
p as
Element of
QC-WFF by A5, ZFMISC_1:33;
All x,
p' = (<*[3,0 ]*> ^ <*x*>) ^ (@ p')
;
hence
[((<*[3,0 ]*> ^ <*x*>) ^ p),e] in [:QC-WFF ,vSUB :]
by ZFMISC_1:def 2;
:: thesis: verum
end;