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) = w | (still_not-bound_in p) 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) = 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 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) = 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 (Al,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 (Al,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 Th63;
then A2: dom ((v . (x | a)) | (still_not-bound_in p)) = dom ((w . (x | a)) | (still_not-bound_in p)) by A1, Th63;
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 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, Th63;
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, Th63;
then A6: v . b = w . b by A1, A5, FUNCT_1:47;
A7: now :: thesis: ( b <> x implies ((v . (x | a)) | (still_not-bound_in p)) . b = ((w . (x | a)) | (still_not-bound_in p)) . b )
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 Th48;
hence ((v . (x | a)) | (still_not-bound_in p)) . b = ((w . (x | a)) | (still_not-bound_in p)) . b by A4, A6, A8, Th48; :: 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 )
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 Th49;
hence ((v . (x | a)) | (still_not-bound_in p)) . b = ((w . (x | a)) | (still_not-bound_in p)) . b by A4, A9, Th49; :: 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