let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for x, y 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 st not y in still_not-bound_in (All (x,p)) holds
((v . (y | a)) . (x | a)) | (still_not-bound_in p) = (v . (x | a)) | (still_not-bound_in p)
let p be Element of CQC-WFF Al; :: thesis: for x, y 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 st not y in still_not-bound_in (All (x,p)) holds
((v . (y | a)) . (x | a)) | (still_not-bound_in p) = (v . (x | a)) | (still_not-bound_in p)
let x, y 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 st not y in still_not-bound_in (All (x,p)) holds
((v . (y | a)) . (x | a)) | (still_not-bound_in p) = (v . (x | a)) | (still_not-bound_in p)
let A be non empty set ; :: thesis: for v being Element of Valuations_in (Al,A)
for a being Element of A st not y in still_not-bound_in (All (x,p)) holds
((v . (y | a)) . (x | a)) | (still_not-bound_in p) = (v . (x | a)) | (still_not-bound_in p)
let v be Element of Valuations_in (Al,A); :: thesis: for a being Element of A st not y in still_not-bound_in (All (x,p)) holds
((v . (y | a)) . (x | a)) | (still_not-bound_in p) = (v . (x | a)) | (still_not-bound_in p)
let a be Element of A; :: thesis: ( not y in still_not-bound_in (All (x,p)) implies ((v . (y | a)) . (x | a)) | (still_not-bound_in p) = (v . (x | a)) | (still_not-bound_in p) )
A1: (v . (y | a)) . (x | a) = v +* ((y | a) +* (x | a)) by FUNCT_4:14;
assume A2: not y in still_not-bound_in (All (x,p)) ; :: thesis: ((v . (y | a)) . (x | a)) | (still_not-bound_in p) = (v . (x | a)) | (still_not-bound_in p)

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

assume A3: x <> y ; :: thesis: ((v . (y | a)) . (x | a)) | (still_not-bound_in p) = (v . (x | a)) | (still_not-bound_in p)
( dom (x | a) = {x} & dom (y | a) = {y} ) ;
then (v . (y | a)) . (x | a) = v +* ((x | a) +* (y | a)) by A1, A3, FUNCT_4:35, ZFMISC_1:11;
then A4: (v . (y | a)) . (x | a) = (v +* (x | a)) +* (y | a) by FUNCT_4:14;
not y in (still_not-bound_in p) \ {x} by A2, QC_LANG3:12;
then not y in still_not-bound_in p by A3, ZFMISC_1:56;
hence ((v . (y | a)) . (x | a)) | (still_not-bound_in p) = (v . (x | a)) | (still_not-bound_in p) by A4, Th26; :: thesis: verum

end;

hence ((v . (y | a)) . (x | a)) | (still_not-bound_in p) = (v . (x | a)) | (still_not-bound_in p) by A1; :: thesis: verum