let it1, it2 be strict ConstructorSignature; :: thesis: ( the carrier' of it1 = {* ,non_op } \/ Constructors & ( for o being OperSymbol of it1 st o is constructor holds
( the ResultSort of it1 . o = o `1 & card (the Arity of it1 . o) = card ((o `2 ) `1 ) ) ) & the carrier' of it2 = {* ,non_op } \/ Constructors & ( for o being OperSymbol of it2 st o is constructor holds
( the ResultSort of it2 . o = o `1 & card (the Arity of it2 . o) = card ((o `2 ) `1 ) ) ) implies it1 = it2 )
assume that
A1: the carrier' of it1 = {* ,non_op } \/ Constructors and
A2: for o being OperSymbol of it1 st o is constructor holds
( the ResultSort of it1 . o = o `1 & card (the Arity of it1 . o) = card ((o `2 ) `1 ) ) and
A3: the carrier' of it2 = {* ,non_op } \/ Constructors and
A4: for o being OperSymbol of it2 st o is constructor holds
( the ResultSort of it2 . o = o `1 & card (the Arity of it2 . o) = card ((o `2 ) `1 ) ) ; :: thesis: it1 = it2
set S = {a_Type ,an_Adj ,a_Term };
set O = {* ,non_op } \/ Constructors ;
A5: ( the carrier of it1 = {a_Type ,an_Adj ,a_Term } & the carrier of it2 = {a_Type ,an_Adj ,a_Term } ) by CONSTRSIGN;

BB: now

let c be Element of Constructors ; :: thesis: ( c <> * & c <> non_op implies the Arity of it1 . c = the Arity of it2 . c )
reconsider o1 = c as OperSymbol of it1 by A1, XBOOLE_0:def 3;
reconsider o2 = o1 as OperSymbol of it2 by A1, A3;
assume B3: ( c <> * & c <> non_op ) ; :: thesis: the Arity of it1 . c = the Arity of it2 . c
then ( o1 is constructor & o2 is constructor ) by CNSTR2;
then B1: ( card (the Arity of it1 . o1) = card ((c `2 ) `1 ) & card (the Arity of it2 . o2) = card ((c `2 ) `1 ) ) by A2, A4;
( the Arity of it1 . o1 in {a_Term } * & the Arity of it2 . o2 in {a_Term } * ) by B3, CONSTRSIGN;
then reconsider p1 = the Arity of it1 . o1, p2 = the Arity of it2 . o2 as FinSequence of {a_Term } by FINSEQ_1:def 11;
B2: ( dom p1 = Seg (len p1) & dom p2 = Seg (len p2) ) by FINSEQ_1:def 3;

now

let i be Nat; :: thesis: ( i in dom p1 implies p1 . i = p2 . i )
assume i in dom p1 ; :: thesis: p1 . i = p2 . i
then ( p1 . i in rng p1 & rng p1 c= {a_Term } & p2 . i in rng p2 & rng p2 c= {a_Term } ) by B1, B2, FUNCT_1:def 5;
then ( p1 . i = a_Term & p2 . i = a_Term ) by TARSKI:def 1;
hence p1 . i = p2 . i ; :: thesis: verum

end;

hence the Arity of it1 . c = the Arity of it2 . c by B1, B2, FINSEQ_1:17; :: thesis: verum

end;

now

let o be OperSymbol of it1; :: thesis: the Arity of it1 . o = the Arity of it2 . o
( o in {* ,non_op } or not o in {* ,non_op } ) ;
then ( o = * or o = non_op or ( o in Constructors & o <> * & o <> non_op ) ) by A1, TARSKI:def 2, XBOOLE_0:def 3;
then ( ( the Arity of it1 . o = <*an_Adj ,a_Type *> & the Arity of it2 . o = <*an_Adj ,a_Type *> ) or ( the Arity of it1 . o = <*an_Adj *> & the Arity of it2 . o = <*an_Adj *> ) or the Arity of it1 . o = the Arity of it2 . o ) by BB, CONSTRSIGN;
hence the Arity of it1 . o = the Arity of it2 . o ; :: thesis: verum

end;

then A6: the Arity of it1 = the Arity of it2 by A1, A3, A5, FUNCT_2:113;

now

let o be OperSymbol of it1; :: thesis: the ResultSort of it1 . o = the ResultSort of it2 . o
reconsider o' = o as OperSymbol of it2 by A1, A3;
( not o in {* ,non_op } or o in {* ,non_op } ) ;
then ( o = * or o = non_op or ( o in Constructors & o is constructor & o' is constructor ) ) by A1, CNSTR2, TARSKI:def 2, XBOOLE_0:def 3;
then ( ( the ResultSort of it1 . o = a_Type & the ResultSort of it2 . o = a_Type ) or ( the ResultSort of it1 . o = an_Adj & the ResultSort of it2 . o = an_Adj ) or ( the ResultSort of it1 . o = o `1 & the ResultSort of it2 . o = o `1 ) ) by A2, A4, CONSTRSIGN;
hence the ResultSort of it1 . o = the ResultSort of it2 . o ; :: thesis: verum

end;

hence it1 = it2 by A6, A1, A3, A5, FUNCT_2:113; :: thesis: verum