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)) | = (v . (x | a)) |

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)) | = (v . (x | a)) |

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)) | = (v . (x | a)) |

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)) | = (v . (x | a)) |

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)) | = (v . (x | a)) |

let a be Element of A; :: thesis: ( not y in still_not-bound_in (All (x,p)) implies ((v . (y | a)) . (x | a)) | = (v . (x | a)) | )
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)) | = (v . (x | a)) |
now :: thesis: ( x <> y implies ((v . (y | a)) . (x | a)) | = (v . (x | a)) | )
assume A3: x <> y ; :: thesis: ((v . (y | a)) . (x | a)) | = (v . (x | a)) |
( dom (x | a) = {x} & dom (y | a) = {y} ) ;
then (v . (y | a)) . (x | a) = v +* ((x | a) +* (y | a)) by ;
then A4: (v . (y | a)) . (x | a) = (v +* (x | a)) +* (y | a) by FUNCT_4:14;
not y in \ {x} by ;
then not y in still_not-bound_in p by ;
hence ((v . (y | a)) . (x | a)) | = (v . (x | a)) | by ; :: thesis: verum
end;
hence ((v . (y | a)) . (x | a)) | = (v . (x | a)) | by A1; :: thesis: verum