:: deftheorem defines Rule3e FOMODEL4:def 27 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule3e Seqts iff ex s being relational Element of S ex T, U being |.(ar b₄).| -element Element of (AllTermsOf S) * st
( seqt `1 = {(s -compound T)} \/ { ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg |.(ar s).|, TT, UU is Function of (Seg |.(ar s).|),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T & UU = U ) } & seqt `2 = s -compound U ) );