theorem Th16: :: CATALG_1:16

for A being non empty set
for o being OperSymbol of (CatSign A) holds
( ( o `1 = 1 & len (o `2) = 1 ) or ( o `1 = 2 & len (o `2) = 3 ) )