theorem Th12: :: ABCMIZ_A:12

for C being initialized ConstructorSignature
for e being expression of C
for o being OperSymbol of C st e . {} = [o, the carrier of C] holds
e is expression of C, the_result_sort_of o