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 a being Element of A
for X being set st X c= bound_QC-variables Al & not x in X holds
(v . (x | a)) | X = v | X

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 a being Element of A
for X being set st X c= bound_QC-variables Al & not x in X holds
(v . (x | a)) | X = v | X

let A be non empty set ; :: thesis: for v being Element of Valuations_in (Al,A)
for a being Element of A
for X being set st X c= bound_QC-variables Al & not x in X holds
(v . (x | a)) | X = v | X

let v be Element of Valuations_in (Al,A); :: thesis: for a being Element of A
for X being set st X c= bound_QC-variables Al & not x in X holds
(v . (x | a)) | X = v | X

let a be Element of A; :: thesis: for X being set st X c= bound_QC-variables Al & not x in X holds
(v . (x | a)) | X = v | X

let X be set ; :: thesis: ( X c= bound_QC-variables Al & not x in X implies (v . (x | a)) | X = v | X )
assume that
A1: X c= bound_QC-variables Al and
A2: not x in X ; :: thesis: (v . (x | a)) | X = v | X
set f2 = v | X;
set f1 = (v . (x | a)) | X;
A3: dom ((v . (x | a)) | X) = dom (v | X) by ;
now :: thesis: for b being object st b in dom ((v . (x | a)) | X) holds
((v . (x | a)) | X) . b = (v | X) . b
let b be object ; :: thesis: ( b in dom ((v . (x | a)) | X) implies ((v . (x | a)) | X) . b = (v | X) . b )
assume A4: b in dom ((v . (x | a)) | X) ; :: thesis: ((v . (x | a)) | X) . b = (v | X) . b
x <> b by A2, A4;
then A5: (v . (x | a)) . b = v . b by SUBLEMMA:48;
(v . (x | a)) . b = ((v . (x | a)) | X) . b by ;
hence ((v . (x | a)) | X) . b = (v | X) . b by ; :: thesis: verum
end;
hence (v . (x | a)) | X = v | X by ; :: thesis: verum