let x be bound_QC-variable; :: thesis: for A being non empty set
for v being Element of Valuations_in A
for vS being Val_Sub of A
for vS1 being Function st ( for y being bound_QC-variable st y in dom vS1 holds
vS1 . y = v . y ) & dom vS misses dom vS1 holds
for y being bound_QC-variable 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 A
for vS being Val_Sub of A
for vS1 being Function st ( for y being bound_QC-variable st y in dom vS1 holds
vS1 . y = v . y ) & dom vS misses dom vS1 holds
for y being bound_QC-variable st y in (dom vS1) \ {x} holds
(vS1 | ((dom vS1) \ {x})) . y = (v . vS) . y
let v be Element of Valuations_in A; :: thesis: for vS being Val_Sub of A
for vS1 being Function st ( for y being bound_QC-variable st y in dom vS1 holds
vS1 . y = v . y ) & dom vS misses dom vS1 holds
for y being bound_QC-variable st y in (dom vS1) \ {x} holds
(vS1 | ((dom vS1) \ {x})) . y = (v . vS) . y
let vS be Val_Sub of A; :: thesis: for vS1 being Function st ( for y being bound_QC-variable st y in dom vS1 holds
vS1 . y = v . y ) & dom vS misses dom vS1 holds
for y being bound_QC-variable 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 st y in dom vS1 holds
vS1 . y = v . y ) & dom vS misses dom vS1 implies for y being bound_QC-variable st y in (dom vS1) \ {x} holds
(vS1 | ((dom vS1) \ {x})) . y = (v . vS) . y )
assume A1: ( ( for y being bound_QC-variable st y in dom vS1 holds
vS1 . y = v . y ) & dom vS misses dom vS1 ) ; :: thesis: for y being bound_QC-variable st y in (dom vS1) \ {x} holds
(vS1 | ((dom vS1) \ {x})) . y = (v . vS) . y
let y be bound_QC-variable; :: thesis: ( y in (dom vS1) \ {x} implies (vS1 | ((dom vS1) \ {x})) . y = (v . vS) . y )
assume A2: y in (dom vS1) \ {x} ; :: thesis: (vS1 | ((dom vS1) \ {x})) . y = (v . vS) . y
y in (dom vS1) /\ ((dom vS1) \ {x}) by A2, XBOOLE_0:def 4;
then (vS1 | ((dom vS1) \ {x})) . y = vS1 . y by FUNCT_1:71;
then A3: (vS1 | ((dom vS1) \ {x})) . y = v . y by A1, A2;
not y in dom vS by A1, A2, XBOOLE_0:3;
hence (vS1 | ((dom vS1) \ {x})) . y = (v . vS) . y by A3, FUNCT_4:12; :: thesis: verum