:: deftheorem defines Rule3d FOMODEL4:def 26 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule3d Seqts iff ex s being low-compounding Element of S ex T, U being |.(ar b₄).| -element Element of (AllTermsOf S) * st
( s is operational & seqt `1 = { ((<*(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 = (<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U) ) );