let S1, S2 be non empty ManySortedSign ; :: thesis: for v being Vertex of S2 holds v is Vertex of (S1 +* S2)
let v be Vertex of S2; :: thesis: v is Vertex of (S1 +* S2)
v in the carrier of S1 \/ the carrier of S2 by XBOOLE_0:def 3;
hence v is Vertex of (S1 +* S2) by CIRCCOMB:def 2; :: thesis: verum