let M be non empty set ; :: thesis: 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
( (Free H1) /\ (Free H2) c= {(x. 3),(x. 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) )
let H1 be ZF-formula; :: thesis: 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
( (Free H1) /\ (Free H2) c= {(x. 3),(x. 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) )
let v1 be Function of VAR,M; :: thesis: ( not x. 0 in Free H1 & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) implies ex H2 being ZF-formula ex v2 being Function of VAR,M st
( (Free H1) /\ (Free H2) c= {(x. 3),(x. 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) ) )
assume that
A1: not x. 0 in Free H1 and
A2: M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) ; :: thesis: ex H2 being ZF-formula ex v2 being Function of VAR,M st
( (Free H1) /\ (Free H2) c= {(x. 3),(x. 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) )
consider i being Element of NAT such that
A3: for j being Element of NAT st x. j in variables_in H1 holds
j < i by Th3;
consider H2 being ZF-formula, v2 being Function of VAR,M such that
A4: for j being Element of NAT st j < i & x. j in variables_in H2 & not j = 3 holds
j = 4 and
A5: not x. 0 in Free H2 and
A6: M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) and
A7: def_func' (H1,v1) = def_func' (H2,v2) by A1, A2, Th16;
take H2 ; :: thesis: ex v2 being Function of VAR,M st
( (Free H1) /\ (Free H2) c= {(x. 3),(x. 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) )
take v2 ; :: thesis: ( (Free H1) /\ (Free H2) c= {(x. 3),(x. 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) )
thus (Free H1) /\ (Free H2) c= {(x. 3),(x. 4)} :: thesis: ( 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) )

proof

A8: Free H2 c= variables_in H2 by ZF_LANG1:151;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (Free H1) /\ (Free H2) or a in {(x. 3),(x. 4)} )
A9: Free H1 c= variables_in H1 by ZF_LANG1:151;
assume A10: a in (Free H1) /\ (Free H2) ; :: thesis: a in {(x. 3),(x. 4)}
then A11: a in Free H2 by XBOOLE_0:def 4;
reconsider x = a as Variable by A10;
consider j being Element of NAT such that
A12: x = x. j by ZF_LANG1:77;
a in Free H1 by A10, XBOOLE_0:def 4;
then ( j = 3 or j = 4 ) by A3, A4, A11, A12, A9, A8;
hence a in {(x. 3),(x. 4)} by A12, TARSKI:def 2; :: thesis: verum

end;

thus ( 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) ) by A5, A6, A7; :: thesis: verum