let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable
for A being non empty set
for v, w being Element of Valuations_in A
for a being Element of A st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
(v . (x | a)) | (still_not-bound_in p) = (w . (x | a)) | (still_not-bound_in p)
let x be bound_QC-variable; :: thesis: for A being non empty set
for v, w being Element of Valuations_in A
for a being Element of A st v | (still_not-bound_in p) = w | (still_not-bound_in p) 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 A
for a being Element of A st v | (still_not-bound_in p) = w | (still_not-bound_in p) 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 A; :: thesis: for a being Element of A st v | (still_not-bound_in p) = w | (still_not-bound_in p) 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) = w | (still_not-bound_in p) implies (v . (x | a)) | (still_not-bound_in p) = (w . (x | a)) | (still_not-bound_in p) )
assume A1: v | (still_not-bound_in p) = w | (still_not-bound_in p) ; :: thesis: (v . (x | a)) | (still_not-bound_in p) = (w . (x | a)) | (still_not-bound_in p)
dom (v | (still_not-bound_in p)) = dom ((v . (x | a)) | (still_not-bound_in p)) by Th64;
then A2: dom ((v . (x | a)) | (still_not-bound_in p)) = dom ((w . (x | a)) | (still_not-bound_in p)) by A1, Th64;
for b being set 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 set ; :: 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 A3: 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
A4: ( ((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, A3, FUNCT_1:47;
b in dom (v | (still_not-bound_in p)) by A3, Th64;
then A5: (v | (still_not-bound_in p)) . b = v . b by FUNCT_1:47;
b in dom (w | (still_not-bound_in p)) by A1, A3, Th64;
then A6: v . b = w . b by A1, A5, FUNCT_1:47;

A7: now

assume A8: b <> x ; :: thesis: ((v . (x | a)) | (still_not-bound_in p)) . b = ((w . (x | a)) | (still_not-bound_in p)) . b
then (v . (x | a)) . b = v . b by Th49;
hence ((v . (x | a)) | (still_not-bound_in p)) . b = ((w . (x | a)) | (still_not-bound_in p)) . b by A4, A6, A8, Th49; :: thesis: verum

end;

now

assume A9: b = x ; :: thesis: ((v . (x | a)) | (still_not-bound_in p)) . b = ((w . (x | a)) | (still_not-bound_in p)) . b
then (v . (x | a)) . b = a by Th50;
hence ((v . (x | a)) | (still_not-bound_in p)) . b = ((w . (x | a)) | (still_not-bound_in p)) . b by A4, A9, Th50; :: thesis: verum

end;

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

end;

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