theorem :: INSTALG1:17

for S1 being 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 #)