theorem :: ALGSPEC1:32

for S being non void Signature
for f being Function holds f, {} form_a_replacement_in S ;