for S1, S2 being non void Signature st S1 tolerates S2 holds
for f, g being Function st f,g form_a_replacement_in S1 +* S2 holds
(S1 +* S2) with-replacement (f,g) = (S1 with-replacement (f,g)) +* (S2 with-replacement (f,g))