(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:129; :: according to ABCMIZ_1:def 27 :: thesis: verum