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 Constructors 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 Constructors 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);
A3: dom (* ,non_op --> <*a,t*>,aa) = {* ,non_op } by FUNCT_4:65;
A4: dom (* ,non_op --> t,a) = {* ,non_op } by FUNCT_4:65;
A5: dom f = Constructors by PARTFUN1:def 4;
A6: dom g = Constructors by PARTFUN1:def 4;
A7: dom (f +* (* ,non_op --> <*a,t*>,aa)) = {* ,non_op } \/ Constructors by A3, A5, FUNCT_4:def 1;
A8: dom (g +* (* ,non_op --> t,a)) = {* ,non_op } \/ Constructors by A4, A6, 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
A9: x in Constructors and
A10: y = f . x by A5, FUNCT_1:def 5;
reconsider x = x as Element of Constructors by A9;
y = (len (loci_of x)) |-> tr by A1, A10;
hence y in {a_Type ,an_Adj ,a_Term } * by FINSEQ_1:def 11; :: thesis:

end;

then A11: (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
A12: x in Constructors and
A13: y = g . x by A6, FUNCT_1:def 5;
reconsider x = x as Element of Constructors by A12;
y = kind_of x by A2, A13;
hence y in {a_Type ,an_Adj ,a_Term } ; :: thesis:

end;

then A14: (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 A7, A11, 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 A8, A14, 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:
A15: * in {* ,non_op } by TARSKI:def 2;
A16: non_op in {* ,non_op } by TARSKI:def 2;
thus the Arity of Max . * = (* ,non_op --> <*a,t*>,aa) . * by A3, A15, 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 A3, A16, FUNCT_4:14
.= <*an_Adj *> by FUNCT_4:66 ; :: thesis:
thus the ResultSort of Max . * = (* ,non_op --> t,a) . * by A4, A15, FUNCT_4:14
.= a_Type by FUNCT_4:66 ; :: thesis:
thus the ResultSort of Max . non_op = (* ,non_op --> t,a) . non_op by A4, A16, FUNCT_4:14
.= an_Adj by FUNCT_4:66 ; :: thesis:
let o be Element of the carrier' of Max; :: thesis:
assume that
A17: o <> * and
A18: o <> non_op ; :: thesis:
A19: not o in {* ,non_op } by A17, A18, 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 A3, A5, A19, 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 that
A20: o <> * and
A21: o <> non_op ; :: according to ABCMIZ_1:def 11 :: thesis:
A22: not o in {* ,non_op } by A20, A21, 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 A4, A6, A22, FUNCT_4:def 1
.= o `1 by A2 ; :: thesis:
thus card (the Arity of Max . o) = card (f . c) by A3, A5, A22, FUNCT_4:def 1
.= card H₂(c) by A1
.= card ((o `2 ) `1 ) by FINSEQ_1:def 18 ; :: thesis: