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 = rng the ResultSort of S1 & InnerVertices S2 = rng the ResultSort of S2 & InnerVertices (S1 +* S2) = rng the ResultSort of (S1 +* S2) ) ;
A4: ( the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 & the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 ) by CIRCCOMB:def 2;
A5: rng the ResultSort of (S1 +* S2) = (rng the ResultSort of S1) \/ (rng the ResultSort of S2) by A1, A3, CIRCCOMB:15;

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

let x be set ; :: thesis: ( x in InputVertices S1 implies x in InputVertices (S1 +* S2) )
assume x in InputVertices S1 ; :: thesis: x in InputVertices (S1 +* S2)
then ( x in the carrier of S1 & 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 ( x in the carrier of (S1 +* S2) & not x in rng the ResultSort of (S1 +* S2) ) by A4, A5, XBOOLE_0:def 3;
hence x in InputVertices (S1 +* S2) by XBOOLE_0:def 5; :: thesis: verum

end;

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

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

let x be set ; :: thesis: ( x in InputVertices (S1 +* S2) implies x in (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) )
assume x in InputVertices (S1 +* S2) ; :: thesis: x in (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1))
then ( x in (InputVertices S1) \/ (InputVertices S2) & not x in rng the ResultSort of (S1 +* S2) ) by A6, XBOOLE_0:def 5;
then ( x in InputVertices S1 or ( x in InputVertices S2 & not x in InnerVertices S1 ) ) by A5, 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 set ; :: 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 ( x in InputVertices S1 or x in (InputVertices S2) \ (rng the ResultSort of S1) ) by XBOOLE_0:def 3;
then ( ( 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, XBOOLE_0:3, XBOOLE_0:def 5;
then ( ( x in the carrier of S1 or x in the carrier of S2 ) & not x in rng the ResultSort of S1 & not x in rng the ResultSort of S2 ) by XBOOLE_0:def 5;
then ( x in the carrier of (S1 +* S2) & not x in rng the ResultSort of (S1 +* S2) ) by A4, A5, XBOOLE_0:def 3;
hence x in InputVertices (S1 +* S2) by XBOOLE_0:def 5; :: thesis: verum