theorem Th58: :: ABCMIZ_1:58

for C being initialized ConstructorSignature
for e being expression of C st e . {} = [*, the carrier of C] holds
ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st e = (ast C) term (a,t)