let S1, S2, E1, E2 be Signature; ( 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 #) & ManySortedSign(# the carrier of E1, the carrier' of E1, the Arity of E1, the ResultSort of E1 #) = ManySortedSign(# the carrier of E2, the carrier' of E2, the Arity of E2, the ResultSort of E2 #) & E1 is Extension of S1 implies E2 is Extension of S2 )
assume A1:
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 #)
; ( not ManySortedSign(# the carrier of E1, the carrier' of E1, the Arity of E1, the ResultSort of E1 #) = ManySortedSign(# the carrier of E2, the carrier' of E2, the Arity of E2, the ResultSort of E2 #) or not E1 is Extension of S1 or E2 is Extension of S2 )
assume A2:
ManySortedSign(# the carrier of E1, the carrier' of E1, the Arity of E1, the ResultSort of E1 #) = ManySortedSign(# the carrier of E2, the carrier' of E2, the Arity of E2, the ResultSort of E2 #)
; ( not E1 is Extension of S1 or E2 is Extension of S2 )
set f = id the carrier of S1;
set g = id the carrier' of S1;
assume A3:
( dom (id the carrier of S1) = the carrier of S1 & dom (id the carrier' of S1) = the carrier' of S1 & rng (id the carrier of S1) c= the carrier of E1 & rng (id the carrier' of S1) c= the carrier' of E1 & (id the carrier of S1) * the ResultSort of S1 = the ResultSort of E1 * (id the carrier' of S1) & ( for o being set
for p being Function st o in the carrier' of S1 & p = the Arity of S1 . o holds
(id the carrier of S1) * p = the Arity of E1 . ((id the carrier' of S1) . o) ) )
; PUA2MSS1:def 12,INSTALG1:def 2,ALGSPEC1:def 5 E2 is Extension of S2
thus
dom (id the carrier of S2) = the carrier of S2
; PUA2MSS1:def 12,INSTALG1:def 2,ALGSPEC1:def 5 ( dom (id the carrier' of S2) = the carrier' of S2 & rng (id the carrier of S2) c= the carrier of E2 & rng (id the carrier' of S2) c= the carrier' of E2 & the ResultSort of S2 * (id the carrier of S2) = (id the carrier' of S2) * the ResultSort of E2 & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of S2 or not b2 = the Arity of S2 . b1 or b2 * (id the carrier of S2) = the Arity of E2 . ((id the carrier' of S2) . b1) ) ) )
thus
( dom (id the carrier' of S2) = the carrier' of S2 & rng (id the carrier of S2) c= the carrier of E2 & rng (id the carrier' of S2) c= the carrier' of E2 & the ResultSort of S2 * (id the carrier of S2) = (id the carrier' of S2) * the ResultSort of E2 & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of S2 or not b2 = the Arity of S2 . b1 or b2 * (id the carrier of S2) = the Arity of E2 . ((id the carrier' of S2) . b1) ) ) )
by A1, A2, A3; verum