let C be 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)
let e be expression of C; ( e . {} = [*, the carrier of C] implies 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) )
assume A1:
e . {} = [*, the carrier of C]
; 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)
ast C in the carrier' of C
;
then A2:
e . {} in [: the carrier' of C,{ the carrier of C}:]
by A1, ZFMISC_1:106;