let S1, S2 be non empty ManySortedSign ; :: thesis: ( S1 tolerates S2 implies for v1 being Vertex of S1 st v1 in InputVertices (S1 +* S2) holds
v1 in InputVertices S1 )
assume that
the Arity of S1 tolerates the Arity of S2 and
A1: the ResultSort of S1 tolerates the ResultSort of S2 ; :: according to CIRCCOMB:def 1 :: thesis: for v1 being Vertex of S1 st v1 in InputVertices (S1 +* S2) holds
v1 in InputVertices S1
set S = S1 +* S2;
set R = the ResultSort of (S1 +* S2);
set R1 = the ResultSort of S1;
set R2 = the ResultSort of S2;
the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 by Def2;
then the ResultSort of S1 c= the ResultSort of (S1 +* S2) by A1, FUNCT_4:28;
then A2: rng the ResultSort of S1 c= rng the ResultSort of (S1 +* S2) by RELAT_1:11;
let v1 be Vertex of S1; :: thesis: ( v1 in InputVertices (S1 +* S2) implies v1 in InputVertices S1 )
assume v1 in InputVertices (S1 +* S2) ; :: thesis: v1 in InputVertices S1
then not v1 in rng the ResultSort of S1 by A2, XBOOLE_0:def 5;
hence v1 in InputVertices S1 by XBOOLE_0:def 5; :: thesis: verum