for E being non empty set st E is epsilon-transitive holds
( ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ) iff for H being ZF-formula
for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of E holds (def_func' (H,f)) .: u in E )