theorem Th2: :: SUBLEMMA:2

for Al being QC-alphabet
for x being bound_QC-variable of Al
for vS1 being Function st x in dom vS1 holds
(vS1 | ((dom vS1) \ {x})) +* (x .--> (vS1 . x)) = vS1