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 A1: ( not x. 0 in Free H1 & 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
A2: 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
A3: for j being Element of NAT st j < i & x. j in variables_in H2 & not j = 3 holds
j = 4 and
A4: ( 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 A1, 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

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (Free H1) /\ (Free H2) or a in {(x. 3),(x. 4)} )
assume A5: a in (Free H1) /\ (Free H2) ; :: thesis: a in {(x. 3),(x. 4)}
then A6: ( a in Free H1 & a in Free H2 & Free H1 c= VAR ) by XBOOLE_0:def 4;
reconsider x = a as Variable by A5;
consider j being Element of NAT such that
A7: x = x. j by ZF_LANG1:87;
( Free H1 c= variables_in H1 & Free H2 c= variables_in H2 ) by ZF_LANG1:164;
then ( j = 3 or j = 4 ) by A2, A3, A6, A7;
hence a in {(x. 3),(x. 4)} by A7, 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 A4; :: thesis: verum