let S1, S2 be non empty ManySortedSign ; :: thesis: for v2 being Vertex of S2 st v2 in InputVertices (S1 +* S2) holds
v2 in InputVertices S2
set R1 = the ResultSort of S1;
set R2 = the ResultSort of S2;
set S = S1 +* S2;
set R = the ResultSort of (S1 +* S2);
let v2 be Vertex of S2; :: thesis: ( v2 in InputVertices (S1 +* S2) implies v2 in InputVertices S2 )
the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 by Def2;
then A1: rng the ResultSort of S2 c= rng the ResultSort of (S1 +* S2) by FUNCT_4:18;
assume v2 in InputVertices (S1 +* S2) ; :: thesis: v2 in InputVertices S2
then not v2 in rng the ResultSort of S2 by A1, XBOOLE_0:def 5;
hence v2 in InputVertices S2 by XBOOLE_0:def 5; :: thesis: verum