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 :: thesis: for o being OperSymbol of S1 holds the Arity of S1 . o = the Arity of S2 . o

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 ) ) ;

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 Def1, 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:63;

now :: thesis: for o being OperSymbol of S1 holds the ResultSort of S1 . o = the ResultSort of S2 . o

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 ) ) ;

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 Def1;
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:63; :: thesis: verum