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) )

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;

( 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

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

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) )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;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

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

for g being Function of VAR,E st ( for y being Variable holds 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;then not x. 0 in {(x. 0),(x. 1),(x. 2)} by A4;

hence contradiction by ENUMSET1:def 1; :: thesis: verum

( 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