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 )
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; :: 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 by A1, Def2;
then A4: InnerVertices S2 c= InnerVertices S by FUNCT_4:18;
hence v in InnerVertices S by A2, A3; :: thesis: 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; :: thesis: verum