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 Th4;
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, Th17;
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:164;
let a be set ; :: 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:164;
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:87;
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