(ast C) term (a,t) = [*, the carrier of C] -tree <*a,t*> by Th46;
then ((ast C) term (a,t)) . {} = [(ast C), the carrier of C] by TREES_4:def 4;
hence ((ast C) term (a,t)) . {} in [: the carrier' of C,{ the carrier of C}:] by ZFMISC_1:106; :: according to ABCMIZ_1:def 27 :: thesis: verum