let S1, S2 be non empty ManySortedSign ; :: thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds
for v being Vertex of S1 holds f . v is Vertex of S2
let f, g be Function; :: thesis: ( f,g form_morphism_between S1,S2 implies for v being Vertex of S1 holds f . v is Vertex of S2 )
assume that
A1: dom f = the carrier of S1 and
dom g = the carrier' of S1 and
A2: rng f c= the carrier of S2 ; :: according to PUA2MSS1:def 12 :: thesis: ( not proj2 g c= the carrier' of S2 or 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 Vertex of S1 holds f . v is Vertex of S2 )

now :: thesis: for v being Vertex of S1 holds f . v in the carrier of S2

let v be Vertex of S1; :: thesis: f . v in the carrier of S2
f . v in rng f by A1, FUNCT_1:def 3;
hence f . v in the carrier of S2 by A2; :: thesis: verum

end;

hence ( not proj2 g c= the carrier' of S2 or 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 Vertex of S1 holds f . v is Vertex of S2 ) ; :: thesis: verum