:: deftheorem Def2 defines -compound FOMODEL3:def 2 :
for S being Language
for s being Element of S
for b₃ being Function of ((((AllSymbolsOf S) *) \ {{}}) *),(((AllSymbolsOf S) *) \ {{}}) holds
( b₃ = s -compound iff for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds b₃ . V = s -compound V );