theorem Th31: :: CIRCTRM1:31

for S1, S2 being non empty non void ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
for v being Gate of S1 holds g . v is Gate of S2