theorem Th16:
for
M being non
empty set for
i being
Element of
NAT for
H1 being
ZF-formula for
v1 being
Function of
VAR,
M st not
x. 0 in Free H1 &
M,
v1 |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) holds
ex
H2 being
ZF-formula ex
v2 being
Function of
VAR,
M st
( ( for
j being
Element of
NAT st
j < i &
x. j in variables_in H2 & not
j = 3 holds
j = 4 ) & not
x. 0 in Free H2 &
M,
v2 |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) &
def_func' (
H1,
v1)
= def_func' (
H2,
v2) )