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