for n being natural non empty number
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b₂ -extension b₁ PC-correct QC-correct QCLangSignature over Union X
for Y being V3() b₄ -tolerating ManySortedSet of the carrier of S
for L being non-empty Language of Y,S st L is subst-correct & Y is ManySortedSubset of the Sorts of L holds
for x, y being Element of Union Y
for a being SortSymbol of S st x in Y . a & y in Y . a holds
for A being Formula of L holds
( (\not A) / (x,y) = \not (A / (x,y)) & ( for B being Formula of L holds
( (A \and B) / (x,y) = (A / (x,y)) \and (B / (x,y)) & (A \or B) / (x,y) = (A / (x,y)) \or (B / (x,y)) & (A \imp B) / (x,y) = (A / (x,y)) \imp (B / (x,y)) & (A \iff B) / (x,y) = (A / (x,y)) \iff (B / (x,y)) & (\true_ L) / (x,y) = \true_ L ) ) )