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 #) )
assume 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 & the carrier of S2 c= the carrier of S1 & the carrier' of S1 c= the carrier' of S2 & the carrier' of S2 c= the carrier' of S1 & the ResultSort of S1 c= the ResultSort of S2 & the ResultSort of S2 c= the ResultSort of S1 & the Arity of S1 c= the Arity of S2 & the Arity of S2 c= the Arity of S1 ) by Th11, Th12;
then ( the carrier of S1 = the carrier of S2 & the carrier' of S1 = the carrier' of S2 & the ResultSort of S1 = the ResultSort of S2 & the Arity of S1 = the Arity of S2 ) by XBOOLE_0:def 10;
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 #) ; :: thesis: verum