:: deftheorem defines PairWiseEq FOMODEL4:def 61 :
for S being Language
for m being non zero Nat
for T, U being b₂ -element Element of (AllTermsOf S) * holds PairWiseEq (T,U) = { ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg m, TT, UU is Function of (Seg m),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T & UU = U ) } ;