set A = {a_Type ,an_Adj ,a_Term };
reconsider t = a_Type , a = an_Adj as Element of {a_Type ,an_Adj ,a_Term } by ENUMSET1:def 1;
reconsider aa = <*a*> as Element of {a_Type ,an_Adj ,a_Term } * ;
set C = ManySortedSign(# {a_Type ,an_Adj ,a_Term },{* ,non_op },(* ,non_op --> <*a,t*>,aa),(* ,non_op --> t,a) #);
reconsider C = ManySortedSign(# {a_Type ,an_Adj ,a_Term },{* ,non_op },(* ,non_op --> <*a,t*>,aa),(* ,non_op --> t,a) #) as non empty non void strict ManySortedSign ;
take C ; :: thesis:
thus ( the carrier of C = {a_Type ,an_Adj ,a_Term } & {* ,non_op } c= the carrier' of C ) ; :: according to ABCMIZ_1:def 9 :: thesis:
thus the Arity of C . * = <*an_Adj ,a_Type *> by FUNCT_4:66; :: thesis:
thus the Arity of C . non_op = <*an_Adj *> by FUNCT_4:66; :: thesis:
thus the ResultSort of C . * = a_Type by FUNCT_4:66; :: thesis:
thus the ResultSort of C . non_op = an_Adj by FUNCT_4:66; :: thesis:
thus ( ( for o being Element of the carrier' of C st o <> * & o <> non_op holds
the Arity of C . o in {a_Term } * ) & the carrier' of C = {* ,non_op } ) by TARSKI:def 2; :: thesis: