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: ( C is constructor & the carrier' of C = {*,non_op} )
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: ( the Arity of C . * = <*an_Adj,a_Type*> & the Arity of C . non_op = <*an_Adj*> & the ResultSort of C . * = a_Type & the ResultSort of C . non_op = an_Adj & ( 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} )
thus the Arity of C . * = <*an_Adj,a_Type*> by FUNCT_4:63; :: thesis: ( the Arity of C . non_op = <*an_Adj*> & the ResultSort of C . * = a_Type & the ResultSort of C . non_op = an_Adj & ( 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} )
thus the Arity of C . non_op = <*an_Adj*> by FUNCT_4:63; :: thesis: ( the ResultSort of C . * = a_Type & the ResultSort of C . non_op = an_Adj & ( 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} )
thus the ResultSort of C . * = a_Type by FUNCT_4:63; :: thesis: ( the ResultSort of C . non_op = an_Adj & ( 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} )
thus the ResultSort of C . non_op = an_Adj by FUNCT_4:63; :: thesis: ( ( 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} )
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: verum