set S = {a_Type ,an_Adj ,a_Term };
set O = {* ,non_op } \/ Constructors ;
deffunc H₂( Element of Constructors ) -> set = (len (loci_of $1)) |-> a_Term ;
consider f being ManySortedSet of such that
A1: for c being Element of Constructors holds f . c = H₂(c) from PBOOLE:sch 5();
deffunc H₃( Element of Constructors ) -> Element of {a_Type ,an_Adj ,a_Term } = kind_of $1;
consider g being ManySortedSet of such that
A2: for c being Element of Constructors holds g . c = H₃(c) from PBOOLE:sch 5();
reconsider t = a_Type , a = an_Adj , tr = a_Term 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 A = f +* (* ,non_op --> <*a,t*>,aa);
set R = g +* (* ,non_op --> t,a);
B0: ( dom (* ,non_op --> <*a,t*>,aa) = {* ,non_op } & dom (* ,non_op --> t,a) = {* ,non_op } & dom f = Constructors & dom g = Constructors ) by FUNCT_4:65, PARTFUN1:def 4;
then A3: ( dom (f +* (* ,non_op --> <*a,t*>,aa)) = {* ,non_op } \/ Constructors & dom (g +* (* ,non_op --> t,a)) = {* ,non_op } \/ Constructors ) by FUNCT_4:def 1;
rng f c= {a_Type ,an_Adj ,a_Term } *

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
then consider x being set such that
B1: ( x in Constructors & y = f . x ) by B0, FUNCT_1:def 5;
reconsider x = x as Element of Constructors by B1;
y = (len (loci_of x)) |-> tr by A1, B1;
hence y in {a_Type ,an_Adj ,a_Term } * by FINSEQ_1:def 11; :: thesis:

end;

then A5: (rng f) \/ (rng (* ,non_op --> <*a,t*>,aa)) c= ({a_Type ,an_Adj ,a_Term } * ) \/ ({a_Type ,an_Adj ,a_Term } * ) by XBOOLE_1:13;
rng g c= {a_Type ,an_Adj ,a_Term }

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng g ; :: thesis:
then consider x being set such that
B2: ( x in Constructors & y = g . x ) by B0, FUNCT_1:def 5;
reconsider x = x as Element of Constructors by B2;
y = kind_of x by A2, B2;
hence y in {a_Type ,an_Adj ,a_Term } ; :: thesis:

end;

then A6: (rng g) \/ (rng (* ,non_op --> t,a)) c= {a_Type ,an_Adj ,a_Term } \/ {a_Type ,an_Adj ,a_Term } by XBOOLE_1:13;
rng (f +* (* ,non_op --> <*a,t*>,aa)) c= (rng f) \/ (rng (* ,non_op --> <*a,t*>,aa)) by FUNCT_4:18;
then reconsider A = f +* (* ,non_op --> <*a,t*>,aa) as Function of ({* ,non_op } \/ Constructors ),({a_Type ,an_Adj ,a_Term } * ) by A3, A5, FUNCT_2:4, XBOOLE_1:1;
rng (g +* (* ,non_op --> t,a)) c= (rng g) \/ (rng (* ,non_op --> t,a)) by FUNCT_4:18;
then reconsider R = g +* (* ,non_op --> t,a) as Function of ({* ,non_op } \/ Constructors ),{a_Type ,an_Adj ,a_Term } by A3, A6, FUNCT_2:4, XBOOLE_1:1;
reconsider Max = ManySortedSign(# {a_Type ,an_Adj ,a_Term },({* ,non_op } \/ Constructors ),A,R #) as non empty non void strict Signature ;
Max is constructor

thus the carrier of Max = {a_Type ,an_Adj ,a_Term } ; :: according to ABCMIZ_1:def 9 :: thesis:
thus {* ,non_op } c= the carrier' of Max by XBOOLE_1:7; :: thesis:
B3: ( * in {* ,non_op } & non_op in {* ,non_op } ) by TARSKI:def 2;
hence the Arity of Max . * = (* ,non_op --> <*a,t*>,aa) . * by B0, FUNCT_4:14
.= <*an_Adj ,a_Type *> by FUNCT_4:66 ;
:: thesis:
thus the Arity of Max . non_op = (* ,non_op --> <*a,t*>,aa) . non_op by B0, B3, FUNCT_4:14
.= <*an_Adj *> by FUNCT_4:66 ; :: thesis:
thus the ResultSort of Max . * = (* ,non_op --> t,a) . * by B0, B3, FUNCT_4:14
.= a_Type by FUNCT_4:66 ; :: thesis:
thus the ResultSort of Max . non_op = (* ,non_op --> t,a) . non_op by B0, B3, FUNCT_4:14
.= an_Adj by FUNCT_4:66 ; :: thesis:
let o be Element of the carrier' of Max; :: thesis:
assume ( o <> * & o <> non_op ) ; :: thesis:
then B4: not o in {* ,non_op } by TARSKI:def 2;
then reconsider c = o as Element of Constructors by XBOOLE_0:def 3;
reconsider tr = tr as Element of {a_Term } by TARSKI:def 1;
the Arity of Max . o = f . c by B0, B4, FUNCT_4:def 1
.= (len (loci_of c)) |-> tr by A1 ;
hence the Arity of Max . o in {a_Term } * by FINSEQ_1:def 11; :: thesis:

end;

then reconsider Max = Max as strict ConstructorSignature ;
take Max ; :: thesis:
thus the carrier' of Max = {* ,non_op } \/ Constructors ; :: thesis:
let o be OperSymbol of Max; :: thesis:
assume ( o <> * & o <> non_op ) ; :: according to ABCMIZ_1:def 11 :: thesis:
then C1: not o in {* ,non_op } by TARSKI:def 2;
then reconsider c = o as Element of Constructors by XBOOLE_0:def 3;
thus the ResultSort of Max . o = g . c by B0, C1, FUNCT_4:def 1
.= o `1 by A2 ; :: thesis:
thus card (the Arity of Max . o) = card (f . c) by B0, C1, FUNCT_4:def 1
.= card H₂(c) by A1
.= card ((o `2 ) `1 ) by FINSEQ_1:def 18 ; :: thesis: