let S1, S2 be standardized ConstructorSignature; :: thesis: ( the carrier' of S1 = the carrier' of S2 implies ManySortedSign(# the carrier of S1,the carrier' of S1,the Arity of S1,the ResultSort of S1 #) = ManySortedSign(# the carrier of S2,the carrier' of S2,the Arity of S2,the ResultSort of S2 #) )
assume A1: the carrier' of S1 = the carrier' of S2 ; :: thesis: ManySortedSign(# the carrier of S1,the carrier' of S1,the Arity of S1,the ResultSort of S1 #) = ManySortedSign(# the carrier of S2,the carrier' of S2,the Arity of S2,the ResultSort of S2 #)
A2: ( the carrier of S1 = 3 & the carrier of S2 = 3 ) by ABCMIZ_1:def 9, YELLOW11:1;

now

let o be OperSymbol of S1; :: thesis: the Arity of S1 . b₁ = the Arity of S2 . b₁
reconsider o2 = o as OperSymbol of S2 by A1;

per cases ( o = * or o = non_op or ( o is constructor & o2 is constructor ) ) by ABCMIZ_1:def 11;

suppose ( o = * or o = non_op ) ; :: thesis: the Arity of S1 . b₁ = the Arity of S2 . b₁

then ( ( the Arity of S1 . o = <*an_Adj *> & the Arity of S2 . o = <*an_Adj *> ) or ( the Arity of S1 . o = <*an_Adj ,a_Type *> & the Arity of S2 . o = <*an_Adj ,a_Type *> ) ) by ABCMIZ_1:def 9;
hence the Arity of S1 . o = the Arity of S2 . o ; :: thesis: verum

end;

suppose ( o is constructor & o2 is constructor ) ; :: thesis: the Arity of S1 . b₁ = the Arity of S2 . b₁

then ( card ((o `2 ) `1 ) = len (the_arity_of o) & card ((o `2 ) `1 ) = len (the_arity_of o2) & the_arity_of o = (len (the_arity_of o)) |-> a_Term & the_arity_of o2 = (len (the_arity_of o2)) |-> a_Term ) by StandardizedDef, ABCMIZ_1:37;
hence the Arity of S1 . o = the_arity_of o2
.= the Arity of S2 . o ;
:: thesis: verum

end;

end;

end;

then A3: the Arity of S1 = the Arity of S2 by A1, A2, FUNCT_2:113;

now

let o be OperSymbol of S1; :: thesis: the ResultSort of S1 . b₁ = the ResultSort of S2 . b₁
reconsider o2 = o as OperSymbol of S2 by A1;

per cases ( o = * or o = non_op or ( o is constructor & o2 is constructor ) ) by ABCMIZ_1:def 11;

suppose ( o = * or o = non_op ) ; :: thesis: the ResultSort of S1 . b₁ = the ResultSort of S2 . b₁

then ( ( the ResultSort of S1 . o = a_Type & the ResultSort of S2 . o = a_Type ) or ( the ResultSort of S1 . o = an_Adj & the ResultSort of S2 . o = an_Adj ) ) by ABCMIZ_1:def 9;
hence the ResultSort of S1 . o = the ResultSort of S2 . o ; :: thesis: verum

end;

suppose ( o is constructor & o2 is constructor ) ; :: thesis: the ResultSort of S1 . b₁ = the ResultSort of S2 . b₁

then ( the_result_sort_of o = o `1 & the_result_sort_of o2 = o `1 ) by StandardizedDef;
hence the ResultSort of S1 . o = the_result_sort_of o2
.= the ResultSort of S2 . o ;
:: thesis: verum

end;

end;

end;

hence ManySortedSign(# the carrier of S1,the carrier' of S1,the Arity of S1,the ResultSort of S1 #) = ManySortedSign(# the carrier of S2,the carrier' of S2,the Arity of S2,the ResultSort of S2 #) by A1, A2, A3, FUNCT_2:113; :: thesis: verum