theorem Th69:
for
Al being
QC-alphabet for
x being
bound_QC-variable of
Al for
A being non
empty set for
v being
Element of
Valuations_in (
Al,
A)
for
S being
Element of
CQC-Sub-WFF Al for
xSQ being
second_Q_comp of
[S,x] for
a being
Element of
A st
[S,x] is
quantifiable holds
((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))