let E be non empty set ; :: thesis: for F being Function st F is_definable_in E holds
F is_parametrically_definable_in E
set f = the 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 the Function of VAR,E ; :: thesis: ( {(x. 0),(x. 1),(x. 2)} misses Free H & E, the Function of VAR,E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & F = def_func' (H, the Function of VAR,E) )

A4: now :: thesis: for a being object st a in {(x. 0),(x. 1),(x. 2)} holds
not a in Free H

let a be object ; :: 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, the Function of VAR,E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & F = def_func' (H, the Function of VAR,E) )
thus A5: E, the Function of VAR,E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) by A2; :: thesis: F = def_func' (H, the Function of VAR,E)
reconsider F1 = F as Function of E,E by A3;

A6: now :: thesis: not x. 0 in Free H

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 <> the Function of VAR,E . 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, the Function of VAR,E) by A6, A5, Def1; :: thesis: verum