theorem Th16: :: ZFMODEL2:16

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