let S1, S2, S be non empty non void Circuit-like ManySortedSign ; :: thesis:
assume A1: S = S1 +* S2 ; :: thesis:
let A1 be non-empty Circuit of S1; :: thesis:
let A2 be non-empty Circuit of S2; :: thesis:
let A be non-empty Circuit of S; :: thesis:
assume that
A2: S1 tolerates S2 and
A3: the Sorts of A1 tolerates the Sorts of A2 and
A4: the Charact of A1 tolerates the Charact of A2 and
A5: A = A1 +* A2 ; :: according to CIRCCOMB:def 3 :: thesis:
let s be State of A; :: thesis:
let v be Vertex of S; :: thesis:

hereby :: thesis:

let s1 be State of A1; :: thesis:
assume A6: s1 = s | the carrier of S1 ; :: thesis:

A7: now :: thesis:

assume v in InnerVertices S1 ; :: thesis:
then reconsider v1 = v as Element of InnerVertices S1 ;
A8: (Following s1) . v1 = (Den ((action_at v1),A1)) . ((action_at v1) depends_on_in s1) by CIRCUIT2:def 5;
v1 in InnerVertices S by A1, A2, Th17;
then A9: (Following s) . v = (Den ((action_at v),A)) . ((action_at v) depends_on_in s) by CIRCUIT2:def 5;
A10: action_at v = action_at v1 by A1, A2, Th17;
then Den ((action_at v1),A1) = Den ((action_at v),A) by A1, A3, A4, A5, Th28;
hence (Following s) . v = (Following s1) . v by A1, A2, A6, A10, A9, A8, Th30; :: thesis:

end;

assume that
A11: v in the carrier of S1 and
A12: v in InputVertices S ; :: thesis:
reconsider v1 = v as Vertex of S1 by A11;
v1 in InputVertices S1 by A1, A2, A12, Th13;
then A13: (Following s1) . v1 = s1 . v1 by CIRCUIT2:def 5;
A14: dom s1 = the carrier of S1 by CIRCUIT1:3;
(Following s) . v = s . v by A12, CIRCUIT2:def 5;
hence (Following s) . v = (Following s1) . v by A6, A13, A14, FUNCT_1:47; :: thesis:

end;

hence ( ( v in InnerVertices S1 or ( v in the carrier of S1 & v in InputVertices S ) ) implies (Following s) . v = (Following s1) . v ) by A7; :: thesis:

end;

let s2 be State of A2; :: thesis:
assume A15: s2 = s | the carrier of S2 ; :: thesis:

A16: now :: thesis:

assume v in InnerVertices S2 ; :: thesis:
then reconsider v2 = v as Element of InnerVertices S2 ;
A17: (Following s2) . v2 = (Den ((action_at v2),A2)) . ((action_at v2) depends_on_in s2) by CIRCUIT2:def 5;
v2 in InnerVertices S by A1, Th15;
then A18: (Following s) . v = (Den ((action_at v),A)) . ((action_at v) depends_on_in s) by CIRCUIT2:def 5;
A19: action_at v = action_at v2 by A1, Th15;
then Den ((action_at v2),A2) = Den ((action_at v),A) by A1, A3, A5, Th27;
hence (Following s) . v = (Following s2) . v by A1, A15, A19, A18, A17, Th29; :: thesis:

end;

assume that
A20: v in the carrier of S2 and
A21: v in InputVertices S ; :: thesis:
reconsider v2 = v as Vertex of S2 by A20;
v2 in InputVertices S2 by A1, A21, Th12;
then A22: (Following s2) . v2 = s2 . v2 by CIRCUIT2:def 5;
A23: dom s2 = the carrier of S2 by CIRCUIT1:3;
(Following s) . v = s . v by A21, CIRCUIT2:def 5;
hence (Following s) . v = (Following s2) . v by A15, A22, A23, FUNCT_1:47; :: thesis:

end;

hence ( ( not v in InnerVertices S2 & not ( v in the carrier of S2 & v in InputVertices S ) ) or (Following s) . v = (Following s2) . v ) by A16; :: thesis: