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 A2, CIRCCOMB:def 2, CIRCUIT1:3;

then s = s2 +* s1 by A4, FUNCT_4:70;

then s = (Following s2) +* s1 by A6

.= (Following s2) +* (Following s1) by A5

.= Following s by A1, A2, A3, A4, CIRCCOMB:33 ;

hence s = Following s ; :: according to CIRCUIT2:def 6 :: thesis: verum

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 A2, CIRCCOMB:def 2, CIRCUIT1:3;

then s = s2 +* s1 by A4, FUNCT_4:70;

then s = (Following s2) +* s1 by A6

.= (Following s2) +* (Following s1) by A5

.= Following s by A1, A2, A3, A4, CIRCCOMB:33 ;

hence s = Following s ; :: according to CIRCUIT2:def 6 :: thesis: verum