:: deftheorem defines subst-forex AOFA_L00:def 37 :
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 holds
( L is subst-forex iff for A being Formula of L
for x being Element of Union X
for s, s1 being SortSymbol of S
for t being Element of L,s st x in X . s1 holds
for y being Element of Union Y st y in Y . s holds
( ( x = y implies ( (\for (x,A)) / (y,t) = \for (x,A) & (\ex (x,A)) / (y,t) = \ex (x,A) ) ) & ( x <> y & x in (vf t) . s1 implies ex z being Element of Union X ex x0, z0 being Element of Union Y st
( x = x0 & z0 = z & z = the Element of ((X . s1) \ ((vf t) . s1)) \ ((vf A) . s1) & (\for (x,A)) / (y,t) = \for (z,((A / (x0,z0)) / (y,t))) & (\ex (x,A)) / (y,t) = \ex (z,((A / (x0,z0)) / (y,t))) ) ) & ( x <> y & x nin (vf t) . s implies ( (\for (x,A)) / (y,t) = \for (x,(A / (y,t))) & (\ex (x,A)) / (y,t) = \ex (x,(A / (y,t))) ) ) ) );