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 A1, SUBLEMMA:63;
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 A4, FUNCT_1:47;
hence ((v . (x | a)) | X) . b = (v | X) . b by A3, A4, A5, FUNCT_1:47; :: thesis: verum
end;
hence (v . (x | a)) | X = v | X by A3, FUNCT_1:2; :: thesis: verum