theorem Th42: :: ABCMIZ_1:42

for C being initialized ConstructorSignature
for o being OperSymbol of C st len (the_arity_of o) = 1 holds
for a being expression of C st ex s being SortSymbol of C st
( s = (the_arity_of o) . 1 & a is expression of C,s ) holds
[o, the carrier of C] -tree <*a*> is expression of C, the_result_sort_of o