:: deftheorem Def18 defines quotient FOMODEL3:def 18 :
for S being Language
for U being non empty set
for E being Equivalence_Relation of U
for I being b₁,b₂ -interpreter-like Function
for b₅ being Function holds
( b₅ = I quotient E iff ( dom b₅ = OwnSymbolsOf S & ( for o being own Element of S holds b₅ . o = (I . o) quotient E ) ) );