theorem
for
M being non
empty set for
H,
H1,
H2 being
ZF-formula for
v being
Function of
VAR,
M st
{(x. 0),(x. 1),(x. 2)} misses Free H1 &
M,
v |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) &
{(x. 0),(x. 1),(x. 2)} misses Free H2 &
M,
v |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) &
{(x. 0),(x. 1),(x. 2)} misses Free H & not
x. 4
in Free H holds
for
FG being
Function st
dom FG = M & ( for
m being
Element of
M holds
( (
M,
v / (
(x. 3),
m)
|= H implies
FG . m = (def_func' (H1,v)) . m ) & (
M,
v / (
(x. 3),
m)
|= 'not' H implies
FG . m = (def_func' (H2,v)) . m ) ) ) holds
FG is_parametrically_definable_in M