let Al be QC-alphabet ; :: thesis: for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for vS being Val_Sub of A,Al
for vS1 being Function st ( for y being bound_QC-variable of Al st y in dom vS1 holds
vS1 . y = v . y ) & dom vS misses dom vS1 holds
for y being bound_QC-variable of Al st y in (dom vS1) \ {x} holds
(vS1 | ((dom vS1) \ {x})) . y = (v . vS) . y
let x be bound_QC-variable of Al; :: thesis: for A being non empty set
for v being Element of Valuations_in (Al,A)
for vS being Val_Sub of A,Al
for vS1 being Function st ( for y being bound_QC-variable of Al st y in dom vS1 holds
vS1 . y = v . y ) & dom vS misses dom vS1 holds
for y being bound_QC-variable of Al st y in (dom vS1) \ {x} holds
(vS1 | ((dom vS1) \ {x})) . y = (v . vS) . y
let A be non empty set ; :: thesis: for v being Element of Valuations_in (Al,A)
for vS being Val_Sub of A,Al
for vS1 being Function st ( for y being bound_QC-variable of Al st y in dom vS1 holds
vS1 . y = v . y ) & dom vS misses dom vS1 holds
for y being bound_QC-variable of Al st y in (dom vS1) \ {x} holds
(vS1 | ((dom vS1) \ {x})) . y = (v . vS) . y
let v be Element of Valuations_in (Al,A); :: thesis: for vS being Val_Sub of A,Al
for vS1 being Function st ( for y being bound_QC-variable of Al st y in dom vS1 holds
vS1 . y = v . y ) & dom vS misses dom vS1 holds
for y being bound_QC-variable of Al st y in (dom vS1) \ {x} holds
(vS1 | ((dom vS1) \ {x})) . y = (v . vS) . y
let vS be Val_Sub of A,Al; :: thesis: for vS1 being Function st ( for y being bound_QC-variable of Al st y in dom vS1 holds
vS1 . y = v . y ) & dom vS misses dom vS1 holds
for y being bound_QC-variable of Al st y in (dom vS1) \ {x} holds
(vS1 | ((dom vS1) \ {x})) . y = (v . vS) . y
let vS1 be Function; :: thesis: ( ( for y being bound_QC-variable of Al st y in dom vS1 holds
vS1 . y = v . y ) & dom vS misses dom vS1 implies for y being bound_QC-variable of Al st y in (dom vS1) \ {x} holds
(vS1 | ((dom vS1) \ {x})) . y = (v . vS) . y )
assume that
A1: for y being bound_QC-variable of Al st y in dom vS1 holds
vS1 . y = v . y and
A2: dom vS misses dom vS1 ; :: thesis: for y being bound_QC-variable of Al st y in (dom vS1) \ {x} holds
(vS1 | ((dom vS1) \ {x})) . y = (v . vS) . y
let y be bound_QC-variable of Al; :: thesis: ( y in (dom vS1) \ {x} implies (vS1 | ((dom vS1) \ {x})) . y = (v . vS) . y )
assume A3: y in (dom vS1) \ {x} ; :: thesis: (vS1 | ((dom vS1) \ {x})) . y = (v . vS) . y
y in (dom vS1) /\ ((dom vS1) \ {x}) by A3, XBOOLE_0:def 4;
then (vS1 | ((dom vS1) \ {x})) . y = vS1 . y by FUNCT_1:48;
then A4: (vS1 | ((dom vS1) \ {x})) . y = v . y by A1, A3;
not y in dom vS by A2, A3, XBOOLE_0:3;
hence (vS1 | ((dom vS1) \ {x})) . y = (v . vS) . y by A4, FUNCT_4:11; :: thesis: verum