let S1, S2 be non empty non void Circuit-like ManySortedSign ; :: thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds
for v1 being Vertex of S1 st v1 in InnerVertices S1 holds
for v2 being Vertex of S2 st v2 = f . v1 holds
action_at v2 = g . (action_at v1)
let f, g be Function; :: thesis: ( f,g form_morphism_between S1,S2 implies for v1 being Vertex of S1 st v1 in InnerVertices S1 holds
for v2 being Vertex of S2 st v2 = f . v1 holds
action_at v2 = g . (action_at v1) )
assume A1: f,g form_morphism_between S1,S2 ; :: thesis: for v1 being Vertex of S1 st v1 in InnerVertices S1 holds
for v2 being Vertex of S2 st v2 = f . v1 holds
action_at v2 = g . (action_at v1)
let v1 be Vertex of S1; :: thesis: ( v1 in InnerVertices S1 implies for v2 being Vertex of S2 st v2 = f . v1 holds
action_at v2 = g . (action_at v1) )
assume A2: v1 in InnerVertices S1 ; :: thesis: for v2 being Vertex of S2 st v2 = f . v1 holds
action_at v2 = g . (action_at v1)
let v2 be Vertex of S2; :: thesis: ( v2 = f . v1 implies action_at v2 = g . (action_at v1) )
assume A3: v2 = f . v1 ; :: thesis: action_at v2 = g . (action_at v1)
reconsider g1 = g . (action_at v1) as Gate of S2 by A1, Th32;
A4: ( dom g = the carrier' of S1 & dom f = the carrier of S1 ) by A1, PUA2MSS1:def 13;
A5: dom the ResultSort of S1 = the carrier' of S1 by FUNCT_2:def 1;
A6: f .: (InnerVertices S1) c= InnerVertices S2 by A1, Th33;
A7: v2 in f .: (InnerVertices S1) by A2, A3, A4, FUNCT_1:def 12;
the_result_sort_of g1 = (the ResultSort of S2 * g) . (action_at v1) by A4, FUNCT_1:23
.= (f * the ResultSort of S1) . (action_at v1) by A1, PUA2MSS1:def 13
.= f . (the_result_sort_of (action_at v1)) by A5, FUNCT_1:23
.= v2 by A2, A3, MSAFREE2:def 7 ;
hence action_at v2 = g . (action_at v1) by A6, A7, MSAFREE2:def 7; :: thesis: verum