let S1, S be non empty non void Circuit-like ManySortedSign ; :: thesis: for S2 being non empty ManySortedSign st S1 tolerates S2 & S = S1 +* S2 holds
for v1 being Vertex of S1 st v1 in InnerVertices S1 holds
for v being Vertex of S st v1 = v holds
( v in InnerVertices S & action_at v = action_at v1 )
let S2 be non empty ManySortedSign ; :: thesis: ( S1 tolerates S2 & S = S1 +* S2 implies for v1 being Vertex of S1 st v1 in InnerVertices S1 holds
for v being Vertex of S st v1 = v holds
( v in InnerVertices S & action_at v = action_at v1 ) )
assume that
A1: S1 tolerates S2 and
A2: S = S1 +* S2 ; :: thesis: for v1 being Vertex of S1 st v1 in InnerVertices S1 holds
for v being Vertex of S st v1 = v holds
( v in InnerVertices S & action_at v = action_at v1 )
let v1 be Vertex of S1; :: thesis: ( v1 in InnerVertices S1 implies for v being Vertex of S st v1 = v holds
( v in InnerVertices S & action_at v = action_at v1 ) )
assume A3: v1 in InnerVertices S1 ; :: thesis: for v being Vertex of S st v1 = v holds
( v in InnerVertices S & action_at v = action_at v1 )
let v be Vertex of S; :: thesis: ( v1 = v implies ( v in InnerVertices S & action_at v = action_at v1 ) )
assume A4: v1 = v ; :: thesis: ( v in InnerVertices S & action_at v = action_at v1 )
InnerVertices S = (InnerVertices S1) \/ (InnerVertices S2) by A1, A2, Th11;
hence A5: v in InnerVertices S by A3, A4, XBOOLE_0:def 3; :: thesis: action_at v = action_at v1
the carrier' of S = the carrier' of S1 \/ the carrier' of S2 by A2, Def2;
then reconsider o = action_at v1 as OperSymbol of S by XBOOLE_0:def 3;
the_result_sort_of (action_at v1) = v1 by A3, MSAFREE2:def 7;
then v = the_result_sort_of o by A1, A2, A4, Th16;
hence action_at v = action_at v1 by A5, MSAFREE2:def 7; :: thesis: verum