theorem Th20: :: ABCMIZ_A:20

for C being initialized standardized ConstructorSignature
for e being expression of C st (e . {}) `1 in Constructors holds
ex o being OperSymbol of C st
( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o )