for L being non trivial Polish-language
for E being Polish-arity-function of L
for s being Substitution of L,E
for F being Polish-WFF of L,E st s = {} holds
Subst (s,F) = F