let S1, S2, E1, E2 be Signature; :: 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 #) & 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 #) ; :: thesis: ( 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 #) ; :: thesis: ( 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) ) ) ; :: according to PUA2MSS1:def 12,INSTALG1:def 2,ALGSPEC1:def 5 :: thesis: E2 is Extension of S2
thus dom (id the carrier of S2) = the carrier of S2 ; :: according to PUA2MSS1:def 12,INSTALG1:def 2,ALGSPEC1:def 5 :: thesis: ( 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 b₁ being set
for b₂ being set holds
( not b₁ in the carrier' of S2 or not b₂ = the Arity of S2 . b₁ or b₂ * (id the carrier of S2) = the Arity of E2 . ((id the carrier' of S2) . b₁) ) ) )
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 b₁ being set
for b₂ being set holds
( not b₁ in the carrier' of S2 or not b₂ = the Arity of S2 . b₁ or b₂ * (id the carrier of S2) = the Arity of E2 . ((id the carrier' of S2) . b₁) ) ) ) by A1, A2, A3; :: thesis: verum