theorem Th69: :: SUBLEMMA:69

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))