:: deftheorem defines preserves_inputs_of CIRCTRM1:def 11 :
for S1, S2 being non empty ManySortedSign
for f being Function holds
( f preserves_inputs_of S1,S2 iff f .: (InputVertices S1) c= InputVertices S2 );