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