let S1 be feasible ManySortedSign ; :: thesis: for S2 being Subsignature of S1 st S1 is Subsignature of S2 holds
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 #)

let S2 be Subsignature of S1; :: thesis: ( S1 is Subsignature 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 #) )
A1: the carrier of S2 c= the carrier of S1 by Th10;
assume A2: S1 is Subsignature 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 #)
then the carrier of S1 c= the carrier of S2 by Th10;
then A3: the carrier of S1 = the carrier of S2 by ;
A4: the carrier' of S2 c= the carrier' of S1 by Th10;
the carrier' of S1 c= the carrier' of S2 by ;
then A5: the carrier' of S1 = the carrier' of S2 by ;
A6: the Arity of S2 c= the Arity of S1 by Th11;
A7: the ResultSort of S2 c= the ResultSort of S1 by Th11;
the ResultSort of S1 c= the ResultSort of S2 by ;
then A8: the ResultSort of S1 = the ResultSort of S2 by ;
the Arity of S1 c= the Arity of S2 by ;
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 ; :: thesis: verum