let Al be QC-alphabet ; :: thesis: 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
let x be bound_QC-variable of Al; :: thesis: for vS1 being Function st x in dom vS1 holds
(vS1 | ((dom vS1) \ {x})) +* (x .--> (vS1 . x)) = vS1
let vS1 be Function; :: thesis: ( x in dom vS1 implies (vS1 | ((dom vS1) \ {x})) +* (x .--> (vS1 . x)) = vS1 )
assume x in dom vS1 ; :: thesis: (vS1 | ((dom vS1) \ {x})) +* (x .--> (vS1 . x)) = vS1
then ( ((dom vS1) \ {x}) \/ {x} = (dom vS1) \/ {x} & {x} c= dom vS1 ) by XBOOLE_1:39, ZFMISC_1:31;
then ((dom vS1) \ {x}) \/ {x} = dom vS1 by XBOOLE_1:12;
hence (vS1 | ((dom vS1) \ {x})) +* (x .--> (vS1 . x)) = vS1 by FUNCT_7:14; :: thesis: verum