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 s being State of C st s1 = s | the carrier of S1 holds

Following s1 = (Following s) | the carrier of S1 )

assume A1: ( InputVertices S1 misses InnerVertices S2 & 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 s being State of C st s1 = s | the carrier of S1 holds

Following s1 = (Following s) | the carrier of S1

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 s being State of C st s1 = s | the carrier of S1 holds

Following s1 = (Following s) | the carrier of S1

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 s being State of C st s1 = s | the carrier of S1 holds

Following s1 = (Following s) | the carrier of S1

let C be non-empty Circuit of S; :: thesis: ( C1 tolerates C2 & C = C1 +* C2 implies for s1 being State of C1

for s being State of C st s1 = s | the carrier of S1 holds

Following s1 = (Following s) | the carrier of S1 )

assume that

A2: C1 tolerates C2 and

A3: C = C1 +* C2 ; :: thesis: for s1 being State of C1

for s being State of C st s1 = s | the carrier of S1 holds

Following s1 = (Following s) | the carrier of S1

let s1 be State of C1; :: thesis: for s being State of C st s1 = s | the carrier of S1 holds

Following s1 = (Following s) | the carrier of S1

let s be State of C; :: thesis: ( s1 = s | the carrier of S1 implies Following s1 = (Following s) | the carrier of S1 )

assume A4: s1 = s | the carrier of S1 ; :: thesis: Following s1 = (Following s) | the carrier of S1

the Sorts of C1 tolerates the Sorts of C2 by A2, CIRCCOMB:def 3;

then reconsider s2 = s | the carrier of S2 as State of C2 by A3, CIRCCOMB:26;

( dom (Following s1) = the carrier of S1 & Following s = (Following s2) +* (Following s1) ) by A1, A2, A3, A4, CIRCCOMB:33, CIRCUIT1:3;

hence Following s1 = (Following s) | the carrier of S1 by FUNCT_4:23; :: 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 s being State of C st s1 = s | the carrier of S1 holds

Following s1 = (Following s) | the carrier of S1 )

assume A1: ( InputVertices S1 misses InnerVertices S2 & 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 s being State of C st s1 = s | the carrier of S1 holds

Following s1 = (Following s) | the carrier of S1

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 s being State of C st s1 = s | the carrier of S1 holds

Following s1 = (Following s) | the carrier of S1

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 s being State of C st s1 = s | the carrier of S1 holds

Following s1 = (Following s) | the carrier of S1

let C be non-empty Circuit of S; :: thesis: ( C1 tolerates C2 & C = C1 +* C2 implies for s1 being State of C1

for s being State of C st s1 = s | the carrier of S1 holds

Following s1 = (Following s) | the carrier of S1 )

assume that

A2: C1 tolerates C2 and

A3: C = C1 +* C2 ; :: thesis: for s1 being State of C1

for s being State of C st s1 = s | the carrier of S1 holds

Following s1 = (Following s) | the carrier of S1

let s1 be State of C1; :: thesis: for s being State of C st s1 = s | the carrier of S1 holds

Following s1 = (Following s) | the carrier of S1

let s be State of C; :: thesis: ( s1 = s | the carrier of S1 implies Following s1 = (Following s) | the carrier of S1 )

assume A4: s1 = s | the carrier of S1 ; :: thesis: Following s1 = (Following s) | the carrier of S1

the Sorts of C1 tolerates the Sorts of C2 by A2, CIRCCOMB:def 3;

then reconsider s2 = s | the carrier of S2 as State of C2 by A3, CIRCCOMB:26;

( dom (Following s1) = the carrier of S1 & Following s = (Following s2) +* (Following s1) ) by A1, A2, A3, A4, CIRCCOMB:33, CIRCUIT1:3;

hence Following s1 = (Following s) | the carrier of S1 by FUNCT_4:23; :: thesis: verum