let S1 be feasible ManySortedSign ; 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; ( 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
; 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 A1, XBOOLE_0:def 10;
A4:
the carrier' of S2 c= the carrier' of S1
by Th10;
the carrier' of S1 c= the carrier' of S2
by A2, Th10;
then A5:
the carrier' of S1 = the carrier' of S2
by A4, XBOOLE_0:def 10;
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 A2, Th11;
then A8:
the ResultSort of S1 = the ResultSort of S2
by A7, XBOOLE_0:def 10;
the Arity of S1 c= the Arity of S2
by A2, Th11;
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 A6, A3, A5, A8, XBOOLE_0:def 10; verum