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:62;
A4: dom ((*,non_op) --> (t,a)) = {*,non_op} by FUNCT_4:62;
A5: dom f = Constructors by PARTFUN1:def 2;
A6: dom g = Constructors by PARTFUN1:def 2;
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 object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
then consider x being object such that
A9: x in Constructors and
A10: y = f . x by A5, FUNCT_1:def 3;
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 object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng g ; :: thesis:
then consider x being object such that
A12: x in Constructors and
A13: y = g . x by A6, FUNCT_1:def 3;
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:17;
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:2, XBOOLE_1:1;
rng (g +* ((*,non_op) --> (t,a))) c= (rng g) \/ (rng ((*,non_op) --> (t,a))) by FUNCT_4:17;
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:2, 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:13
.= <*an_Adj,a_Type*> by FUNCT_4:63 ; :: thesis:
thus the Arity of Max . non_op = ((*,non_op) --> (<*a,t*>,aa)) . non_op by A3, A16, FUNCT_4:13
.= <*an_Adj*> by FUNCT_4:63 ; :: thesis:
thus the ResultSort of Max . * = ((*,non_op) --> (t,a)) . * by A4, A15, FUNCT_4:13
.= a_Type by FUNCT_4:63 ; :: thesis:
thus the ResultSort of Max . non_op = ((*,non_op) --> (t,a)) . non_op by A4, A16, FUNCT_4:13
.= an_Adj by FUNCT_4:63 ; :: 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 CARD_1:def 7 ; :: thesis: