let E be non empty set ; :: thesis: for F being Function st F is_definable_in E holds
F is_parametrically_definable_in E
consider f being Function of VAR ,E;
let F be Function; :: thesis: ( F is_definable_in E implies F is_parametrically_definable_in E )
given H being ZF-formula such that A1: Free H c= {(x. 3),(x. 4)} and
A2: E |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) and
A3: F = def_func H,E ; :: according to ZFMODEL1:def 3 :: thesis: F is_parametrically_definable_in E
take H ; :: according to ZFMODEL1:def 4 :: thesis: 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 )
take f ; :: thesis: ( {(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 )

A4: now

let a be set ; :: thesis: ( a in {(x. 0 ),(x. 1),(x. 2)} implies not a in Free H )
assume a in {(x. 0 ),(x. 1),(x. 2)} ; :: thesis: not a in Free H
then ( a <> x. 3 & a <> x. 4 ) by ENUMSET1:def 1;
hence not a in Free H by A1, TARSKI:def 2; :: thesis: verum

end;

hence {(x. 0 ),(x. 1),(x. 2)} misses Free H by XBOOLE_0:3; :: thesis: ( E,f |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) & F = def_func' H,f )
thus A5: E,f |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) by A2, ZF_MODEL:def 5; :: thesis: F = def_func' H,f
reconsider F1 = F as Function of E,E by A3;

A6: now

assume x. 0 in Free H ; :: thesis: contradiction
then not x. 0 in {(x. 0 ),(x. 1),(x. 2)} by A4;
hence contradiction by ENUMSET1:def 1; :: thesis: verum

end;

for g being Function of VAR ,E st ( for y being Variable holds
( not g . y <> f . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds
( E,g |= H iff F1 . (g . (x. 3)) = g . (x. 4) ) by A1, A2, A3, Def2;
hence F = def_func' H,f by A6, A5, Def1; :: thesis: verum