let S1, S2 be non empty ManySortedSign ; :: thesis: ( S1 tolerates S2 & InnerVertices S2 misses InputVertices S1 implies ( InputVertices S1 c= InputVertices (S1 +* S2) & InputVertices (S1 +* S2) = (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) ) )
set S = S1 +* S2;
set R = the ResultSort of (S1 +* S2);
set R1 = the ResultSort of S1;
set R2 = the ResultSort of S2;
assume that
A1: S1 tolerates S2 and
A2: InnerVertices S2 misses InputVertices S1 ; :: thesis: ( InputVertices S1 c= InputVertices (S1 +* S2) & InputVertices (S1 +* S2) = (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) )
A3: InnerVertices (S1 +* S2) = rng the ResultSort of (S1 +* S2) ;
( InnerVertices S1 = rng the ResultSort of S1 & InnerVertices S2 = rng the ResultSort of S2 ) ;
then A4: rng the ResultSort of (S1 +* S2) = (rng the ResultSort of S1) \/ (rng the ResultSort of S2) by A1, A3, CIRCCOMB:11;
A5: the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 by CIRCCOMB:def 2;

hereby :: according to TARSKI:def 3 :: thesis: InputVertices (S1 +* S2) = (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1))

let x be object ; :: thesis: ( x in InputVertices S1 implies x in InputVertices (S1 +* S2) )
assume A6: x in InputVertices S1 ; :: thesis: x in InputVertices (S1 +* S2)
then ( not x in rng the ResultSort of S1 & not x in rng the ResultSort of S2 ) by A2, XBOOLE_0:3, XBOOLE_0:def 5;
then A7: not x in rng the ResultSort of (S1 +* S2) by A4, XBOOLE_0:def 3;
x in the carrier of (S1 +* S2) by A5, A6, XBOOLE_0:def 3;
hence x in InputVertices (S1 +* S2) by A7, XBOOLE_0:def 5; :: thesis: verum

end;

A8: InputVertices (S1 +* S2) c= (InputVertices S1) \/ (InputVertices S2) by A1, CIRCCOMB:11;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) c= InputVertices (S1 +* S2)

let x be object ; :: thesis: ( x in InputVertices (S1 +* S2) implies x in (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) )
assume A9: x in InputVertices (S1 +* S2) ; :: thesis: x in (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1))
then not x in rng the ResultSort of (S1 +* S2) by XBOOLE_0:def 5;
then ( x in InputVertices S1 or ( x in InputVertices S2 & not x in InnerVertices S1 ) ) by A4, A8, A9, XBOOLE_0:def 3;
then ( x in InputVertices S1 or x in (InputVertices S2) \ (InnerVertices S1) ) by XBOOLE_0:def 5;
hence x in (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) by XBOOLE_0:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) or x in InputVertices (S1 +* S2) )
assume x in (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) ; :: thesis: x in InputVertices (S1 +* S2)
then A10: ( x in InputVertices S1 or x in (InputVertices S2) \ (rng the ResultSort of S1) ) by XBOOLE_0:def 3;
then A11: x in the carrier of (S1 +* S2) by A5, XBOOLE_0:def 3;
( ( x in InputVertices S1 & not x in rng the ResultSort of S2 ) or ( x in InputVertices S2 & not x in rng the ResultSort of S1 ) ) by A2, A10, XBOOLE_0:3, XBOOLE_0:def 5;
then A12: not x in rng the ResultSort of S2 by XBOOLE_0:def 5;
not x in rng the ResultSort of S1 by A10, XBOOLE_0:def 5;
then not x in rng the ResultSort of (S1 +* S2) by A4, A12, XBOOLE_0:def 3;
hence x in InputVertices (S1 +* S2) by A11, XBOOLE_0:def 5; :: thesis: verum