let S1, S2 be non empty ManySortedSign ; :: thesis: ( S1 tolerates S2 implies InputVertices (S1 +* S2) = ((InputVertices S1) \ (InnerVertices S2)) \/ ((InputVertices S2) \ (InnerVertices S1)) )
A1: the carrier of S1 \ ((rng the ResultSort of S1) \/ (rng the ResultSort of S2)) = (InputVertices S1) \ (InnerVertices S2) by XBOOLE_1:41;
assume S1 tolerates S2 ; :: thesis: InputVertices (S1 +* S2) = ((InputVertices S1) \ (InnerVertices S2)) \/ ((InputVertices S2) \ (InnerVertices S1))
then A2: the ResultSort of S1 tolerates the ResultSort of S2 by CIRCCOMB:def 1;
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 A2, FRECHET:35
.= ( 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 ;
hence InputVertices (S1 +* S2) = ((InputVertices S1) \ (InnerVertices S2)) \/ ((InputVertices S2) \ (InnerVertices S1)) by A1, XBOOLE_1:41; :: thesis: verum