let S1, S2 be non empty ManySortedSign ; :: thesis: ( S1 tolerates S2 implies InputVertices (S1 +* S2) = ((InputVertices S1) \ (InnerVertices S2)) \/ ((InputVertices S2) \ (InnerVertices S1)) )
assume S1 tolerates S2 ; :: thesis: InputVertices (S1 +* S2) = ((InputVertices S1) \ (InnerVertices S2)) \/ ((InputVertices S2) \ (InnerVertices S1))
then A1: the ResultSort of S1 tolerates the ResultSort of S2 by CIRCCOMB:def 1;
A2: InputVertices (S1 +* S2) = the carrier of (S1 +* S2) \ (rng (the ResultSort of S1 +* the ResultSort of S2)) by CIRCCOMB:def 2
.= (the carrier of S1 \/ the carrier of S2) \ (rng (the ResultSort of S1 +* the ResultSort of S2)) by CIRCCOMB:def 2
.= (the carrier of S1 \/ the carrier of S2) \ ((rng the ResultSort of S1) \/ (rng the ResultSort of S2)) by A1, FRECHET:39
.= (the carrier of S1 \ ((rng the ResultSort of S1) \/ (rng the ResultSort of S2))) \/ (the carrier of S2 \ ((rng the ResultSort of S1) \/ (rng the ResultSort of S2))) by XBOOLE_1:42 ;
the carrier of S1 \ ((rng the ResultSort of S1) \/ (rng the ResultSort of S2)) = (InputVertices S1) \ (InnerVertices S2) by XBOOLE_1:41;
hence InputVertices (S1 +* S2) = ((InputVertices S1) \ (InnerVertices S2)) \/ ((InputVertices S2) \ (InnerVertices S1)) by A2, XBOOLE_1:41; :: thesis: verum