theorem Th39: :: ABCMIZ_A:39

for C being initialized ConstructorSignature
for o being nullary OperSymbol of C holds [o, the carrier of C] -tree {} is expression of C, the_result_sort_of o