let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for A being non empty set
for v, w being Element of Valuations_in (Al,A)
for a being Element of A st v | ((still_not-bound_in p) \ {x}) = w | ((still_not-bound_in p) \ {x}) holds
(v . (x | a)) | (still_not-bound_in p) = (w . (x | a)) | (still_not-bound_in p)
let p be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al
for A being non empty set
for v, w being Element of Valuations_in (Al,A)
for a being Element of A st v | ((still_not-bound_in p) \ {x}) = w | ((still_not-bound_in p) \ {x}) holds
(v . (x | a)) | (still_not-bound_in p) = (w . (x | a)) | (still_not-bound_in p)
let x be bound_QC-variable of Al; :: thesis: for A being non empty set
for v, w being Element of Valuations_in (Al,A)
for a being Element of A st v | ((still_not-bound_in p) \ {x}) = w | ((still_not-bound_in p) \ {x}) holds
(v . (x | a)) | (still_not-bound_in p) = (w . (x | a)) | (still_not-bound_in p)
let A be non empty set ; :: thesis: for v, w being Element of Valuations_in (Al,A)
for a being Element of A st v | ((still_not-bound_in p) \ {x}) = w | ((still_not-bound_in p) \ {x}) holds
(v . (x | a)) | (still_not-bound_in p) = (w . (x | a)) | (still_not-bound_in p)
let v, w be Element of Valuations_in (Al,A); :: thesis: for a being Element of A st v | ((still_not-bound_in p) \ {x}) = w | ((still_not-bound_in p) \ {x}) holds
(v . (x | a)) | (still_not-bound_in p) = (w . (x | a)) | (still_not-bound_in p)
let a be Element of A; :: thesis: ( v | ((still_not-bound_in p) \ {x}) = w | ((still_not-bound_in p) \ {x}) implies (v . (x | a)) | (still_not-bound_in p) = (w . (x | a)) | (still_not-bound_in p) )
A1: dom ((w . (x | a)) | (still_not-bound_in p)) = still_not-bound_in p by Th63;
then A2: dom ((v . (x | a)) | (still_not-bound_in p)) = dom ((w . (x | a)) | (still_not-bound_in p)) by Th63;
assume A3: v | ((still_not-bound_in p) \ {x}) = w | ((still_not-bound_in p) \ {x}) ; :: thesis: (v . (x | a)) | (still_not-bound_in p) = (w . (x | a)) | (still_not-bound_in p)
for b being object st b in dom ((v . (x | a)) | (still_not-bound_in p)) holds
((v . (x | a)) | (still_not-bound_in p)) . b = ((w . (x | a)) | (still_not-bound_in p)) . b

proof

let b be object ; :: thesis: ( b in dom ((v . (x | a)) | (still_not-bound_in p)) implies ((v . (x | a)) | (still_not-bound_in p)) . b = ((w . (x | a)) | (still_not-bound_in p)) . b )
assume A4: b in dom ((v . (x | a)) | (still_not-bound_in p)) ; :: thesis: ((v . (x | a)) | (still_not-bound_in p)) . b = ((w . (x | a)) | (still_not-bound_in p)) . b
A5: ( ((v . (x | a)) | (still_not-bound_in p)) . b = (v . (x | a)) . b & ((w . (x | a)) | (still_not-bound_in p)) . b = (w . (x | a)) . b ) by A2, A4, FUNCT_1:47;

A6: now :: thesis: ( b <> x implies ((v . (x | a)) | (still_not-bound_in p)) . b = ((w . (x | a)) | (still_not-bound_in p)) . b )

assume A7: b <> x ; :: thesis: ((v . (x | a)) | (still_not-bound_in p)) . b = ((w . (x | a)) | (still_not-bound_in p)) . b
then A8: not b in {x} by TARSKI:def 1;
b in still_not-bound_in p by A4, Th63;
then A9: b in (still_not-bound_in p) \ {x} by A8, XBOOLE_0:def 5;
then b in dom (w | ((still_not-bound_in p) \ {x})) by Th63;
then A10: (w | ((still_not-bound_in p) \ {x})) . b = w . b by FUNCT_1:47;
A11: ( (v . (x | a)) . b = v . b & (w . (x | a)) . b = w . b ) by A7, Th48;
b in dom (v | ((still_not-bound_in p) \ {x})) by A9, Th63;
hence ((v . (x | a)) | (still_not-bound_in p)) . b = ((w . (x | a)) | (still_not-bound_in p)) . b by A3, A5, A10, A11, FUNCT_1:47; :: thesis: verum

end;

now :: thesis: ( b = x implies ((v . (x | a)) | (still_not-bound_in p)) . b = ((w . (x | a)) | (still_not-bound_in p)) . b )

A12: ((w . (x | a)) | (still_not-bound_in p)) . b = (w . (x | a)) . b by A2, A4, FUNCT_1:47;
assume A13: b = x ; :: thesis: ((v . (x | a)) | (still_not-bound_in p)) . b = ((w . (x | a)) | (still_not-bound_in p)) . b
((v . (x | a)) | (still_not-bound_in p)) . b = (v . (x | a)) . b by A4, FUNCT_1:47;
then ((v . (x | a)) | (still_not-bound_in p)) . b = a by A13, Th49;
hence ((v . (x | a)) | (still_not-bound_in p)) . b = ((w . (x | a)) | (still_not-bound_in p)) . b by A13, A12, Th49; :: thesis: verum

end;

hence ((v . (x | a)) | (still_not-bound_in p)) . b = ((w . (x | a)) | (still_not-bound_in p)) . b by A6; :: thesis: verum

end;

hence (v . (x | a)) | (still_not-bound_in p) = (w . (x | a)) | (still_not-bound_in p) by A1, Th63, FUNCT_1:2; :: thesis: verum