let S1 be non empty ManySortedSign ; 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 ; ( 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
; 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; ( 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
; for v being Vertex of S st v2 = v holds
( v in InnerVertices S & action_at v = action_at v2 )
the carrier' of S = the carrier' of S1 \/ the carrier' of S2
by A1, Def2;
then reconsider o = action_at v2 as OperSymbol of S by XBOOLE_0:def 3;
let v be Vertex of S; ( v2 = v implies ( v in InnerVertices S & action_at v = action_at v2 ) )
assume A3:
v2 = v
; ( v in InnerVertices S & action_at v = action_at v2 )
the ResultSort of S = the ResultSort of S1 +* the ResultSort of S2
by A1, Def2;
then A4:
InnerVertices S2 c= InnerVertices S
by FUNCT_4:18;
hence
v in InnerVertices S
by A2, A3; action_at v = action_at v2
the_result_sort_of (action_at v2) = v2
by A2, MSAFREE2:def 7;
then
v = the_result_sort_of o
by A1, A3, Th14;
hence
action_at v = action_at v2
by A2, A3, A4, MSAFREE2:def 7; verum