let S1, S2, S be non empty non void Circuit-like ManySortedSign ; :: thesis: ( InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 implies for C1 being non-empty Circuit of S1
for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s2 being State of C2
for s being State of C st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable & s2 is stable holds
s is stable )

assume that
A1: InputVertices S1 misses InnerVertices S2 and
A2: S = S1 +* S2 ; :: thesis: for C1 being non-empty Circuit of S1
for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s2 being State of C2
for s being State of C st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable & s2 is stable holds
s is stable

let C1 be non-empty Circuit of S1; :: thesis: for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s2 being State of C2
for s being State of C st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable & s2 is stable holds
s is stable

let C2 be non-empty Circuit of S2; :: thesis: for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s2 being State of C2
for s being State of C st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable & s2 is stable holds
s is stable

let C be non-empty Circuit of S; :: thesis: ( C1 tolerates C2 & C = C1 +* C2 implies for s1 being State of C1
for s2 being State of C2
for s being State of C st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable & s2 is stable holds
s is stable )

assume A3: ( C1 tolerates C2 & C = C1 +* C2 ) ; :: thesis: for s1 being State of C1
for s2 being State of C2
for s being State of C st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable & s2 is stable holds
s is stable

let s1 be State of C1; :: thesis: for s2 being State of C2
for s being State of C st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable & s2 is stable holds
s is stable

let s2 be State of C2; :: thesis: for s being State of C st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable & s2 is stable holds
s is stable

let s be State of C; :: thesis: ( s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable & s2 is stable implies s is stable )
assume that
A4: ( s1 = s | the carrier of S1 & s2 = s | the carrier of S2 ) and
A5: s1 is stable and
A6: s2 is stable ; :: thesis: s is stable
( dom s = the carrier of S & the carrier of S = the carrier of S1 \/ the carrier of S2 ) by ;
then s = s2 +* s1 by ;
then s = () +* s1 by A6
.= () +* () by A5
.= Following s by ;
hence s = Following s ; :: according to CIRCUIT2:def 6 :: thesis: verum