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

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

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