let S1, S2 be non empty ManySortedSign ; ( S1 tolerates S2 implies ( InnerVertices (S1 +* S2) = (InnerVertices S1) \/ (InnerVertices S2) & InputVertices (S1 +* S2) c= (InputVertices S1) \/ (InputVertices S2) ) )
set R1 = the ResultSort of S1;
set R2 = the ResultSort of S2;
assume that
the Arity of S1 tolerates the Arity of S2
and
A1:
the ResultSort of S1 tolerates the ResultSort of S2
; CIRCCOMB:def 1 ( InnerVertices (S1 +* S2) = (InnerVertices S1) \/ (InnerVertices S2) & InputVertices (S1 +* S2) c= (InputVertices S1) \/ (InputVertices S2) )
set S = S1 +* S2;
set R = the ResultSort of (S1 +* S2);
A2:
the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2
by Def2;
then
the ResultSort of S1 c= the ResultSort of (S1 +* S2)
by A1, FUNCT_4:28;
then A3:
rng the ResultSort of S1 c= rng the ResultSort of (S1 +* S2)
by RELAT_1:11;
rng the ResultSort of S2 c= rng the ResultSort of (S1 +* S2)
by A2, FUNCT_4:18;
then A4:
(rng the ResultSort of S1) \/ (rng the ResultSort of S2) c= rng the ResultSort of (S1 +* S2)
by A3, XBOOLE_1:8;
A5:
rng the ResultSort of (S1 +* S2) c= (rng the ResultSort of S1) \/ (rng the ResultSort of S2)
by A2, FUNCT_4:17;
hence
InnerVertices (S1 +* S2) = (InnerVertices S1) \/ (InnerVertices S2)
by A4; InputVertices (S1 +* S2) c= (InputVertices S1) \/ (InputVertices S2)
let x be object ; TARSKI:def 3 ( not x in InputVertices (S1 +* S2) or x in (InputVertices S1) \/ (InputVertices S2) )
assume A6:
x in InputVertices (S1 +* S2)
; x in (InputVertices S1) \/ (InputVertices S2)
then A7:
not x in rng the ResultSort of (S1 +* S2)
by XBOOLE_0:def 5;
A8:
rng the ResultSort of (S1 +* S2) = (rng the ResultSort of S1) \/ (rng the ResultSort of S2)
by A5, A4;
then A9:
not x in rng the ResultSort of S2
by A7, XBOOLE_0:def 3;
the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2
by Def2;
then A10:
( x in the carrier of S1 or x in the carrier of S2 )
by A6, XBOOLE_0:def 3;
not x in rng the ResultSort of S1
by A8, A7, XBOOLE_0:def 3;
then
( x in the carrier of S1 \ (rng the ResultSort of S1) or x in the carrier of S2 \ (rng the ResultSort of S2) )
by A10, A9, XBOOLE_0:def 5;
hence
x in (InputVertices S1) \/ (InputVertices S2)
by XBOOLE_0:def 3; verum