let S1, S2 be non empty non void Circuit-like ManySortedSign ; 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; ( 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
; 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; ( 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
; for v2 being Vertex of S2 st v2 = f . v1 holds
action_at v2 = g . (action_at v1)
let v2 be Vertex of S2; ( v2 = f . v1 implies action_at v2 = g . (action_at v1) )
assume A3:
v2 = f . v1
; action_at v2 = g . (action_at v1)
reconsider g1 = g . (action_at v1) as Gate of S2 by A1, Th31;
A4:
dom g = the carrier' of S1
by A1;
A5:
dom f = the carrier of S1
by A1;
A6:
dom the ResultSort of S1 = the carrier' of S1
by FUNCT_2:def 1;
A7:
f .: (InnerVertices S1) c= InnerVertices S2
by A1, Th32;
A8:
v2 in f .: (InnerVertices S1)
by A2, A3, A5, FUNCT_1:def 6;
the_result_sort_of g1 =
( the ResultSort of S2 * g) . (action_at v1)
by A4, FUNCT_1:13
.=
(f * the ResultSort of S1) . (action_at v1)
by A1
.=
f . (the_result_sort_of (action_at v1))
by A6, FUNCT_1:13
.=
v2
by A2, A3, MSAFREE2:def 7
;
hence
action_at v2 = g . (action_at v1)
by A7, A8, MSAFREE2:def 7; verum