let S1, S2 be non empty non void ManySortedSign ; :: thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds
for v being Gate of S1 holds g . v is Gate of S2
let f, g be Function; :: thesis: ( f,g form_morphism_between S1,S2 implies for v being Gate of S1 holds g . v is Gate of S2 )
assume A1: ( dom f = the carrier of S1 & dom g = the carrier' of S1 & rng f c= the carrier of S2 & rng g c= the carrier' of S2 ) ; :: according to PUA2MSS1:def 13 :: thesis: ( not the ResultSort of S1 * f = g * the ResultSort of S2 or ex b₁ being set ex b₂ being set st
( b₁ in the carrier' of S1 & b₂ = the Arity of S1 . b₁ & not b₂ * f = the Arity of S2 . (g . b₁) ) or for v being Gate of S1 holds g . v is Gate of S2 )

now

let v be Gate of S1; :: thesis: g . v in the carrier' of S2
g . v in rng g by A1, FUNCT_1:def 5;
hence g . v in the carrier' of S2 by A1; :: thesis: verum

end;

hence ( not the ResultSort of S1 * f = g * the ResultSort of S2 or ex b₁ being set ex b₂ being set st
( b₁ in the carrier' of S1 & b₂ = the Arity of S1 . b₁ & not b₂ * f = the Arity of S2 . (g . b₁) ) or for v being Gate of S1 holds g . v is Gate of S2 ) ; :: thesis: verum