:: deftheorem Def4 defines is_parametrically_definable_in ZFMODEL1:def 4 :
for F being Function
for E being non empty set holds
( F is_parametrically_definable_in E iff ex H being ZF-formula ex 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)))))))) & F = def_func' (H,f) ) );