let S1, S2, S be non empty non void Circuit-like ManySortedSign ; :: thesis: ( InnerVertices S1 misses InputVertices 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 s2 being State of C2
for s being State of C st s2 = s | the carrier of S2 holds
Following s2 = (Following s) | the carrier of S2 )
assume A1: ( InnerVertices S1 misses InputVertices 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 s2 being State of C2
for s being State of C st s2 = s | the carrier of S2 holds
Following s2 = (Following s) | the carrier of S2
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 s2 being State of C2
for s being State of C st s2 = s | the carrier of S2 holds
Following s2 = (Following s) | the carrier of S2
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 s2 being State of C2
for s being State of C st s2 = s | the carrier of S2 holds
Following s2 = (Following s) | the carrier of S2
let C be non-empty Circuit of S; :: thesis: ( C1 tolerates C2 & C = C1 +* C2 implies for s2 being State of C2
for s being State of C st s2 = s | the carrier of S2 holds
Following s2 = (Following s) | the carrier of S2 )
assume A2: ( C1 tolerates C2 & C = C1 +* C2 ) ; :: thesis: for s2 being State of C2
for s being State of C st s2 = s | the carrier of S2 holds
Following s2 = (Following s) | the carrier of S2
let s2 be State of C2; :: thesis: for s being State of C st s2 = s | the carrier of S2 holds
Following s2 = (Following s) | the carrier of S2
let s be State of C; :: thesis: ( s2 = s | the carrier of S2 implies Following s2 = (Following s) | the carrier of S2 )
assume A3: s2 = s | the carrier of S2 ; :: thesis: Following s2 = (Following s) | the carrier of S2
A4: dom (Following s2) = the carrier of S2 by CIRCUIT1:4;
the Sorts of C1 tolerates the Sorts of C2 by A2, CIRCCOMB:def 3;
then reconsider s1 = s | the carrier of S1 as State of C1 by A2, CIRCCOMB:33;
Following s = (Following s1) +* (Following s2) by A1, A2, A3, CIRCCOMB:39;
hence Following s2 = (Following s) | the carrier of S2 by A4, FUNCT_4:24; :: thesis: verum