let H be ZF-formula; :: thesis: for M being non empty set
for v being Function of VAR ,M st M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) & not x. 4 in Free H holds
for m being Element of M holds (def_func' H,v) .: m = {}
let M be non empty set ; :: thesis: for v being Function of VAR ,M st M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) & not x. 4 in Free H holds
for m being Element of M holds (def_func' H,v) .: m = {}
let v be Function of VAR ,M; :: thesis: ( M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) & not x. 4 in Free H implies for m being Element of M holds (def_func' H,v) .: m = {} )
assume A1: ( M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) & not x. 4 in Free H ) ; :: thesis: for m being Element of M holds (def_func' H,v) .: m = {}
A2: ( x. 4 <> x. 3 & x. 4 <> x. 0 & x. 3 <> x. 0 ) by ZF_LANG1:86;
consider m3 being Element of M;
M,v / (x. 3),m3 |= Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 )))) by A1, ZF_LANG1:80;
then consider m0 being Element of M such that
A3: M,(v / (x. 3),m3) / (x. 0 ),m0 |= All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))) by ZF_LANG1:82;
set f = (v / (x. 3),m3) / (x. 0 ),m0;

A4: now

let m4 be Element of M; :: thesis: ( M,(v / (x. 3),m3) / (x. 0 ),m0 |= H iff m4 = m0 )
M,((v / (x. 3),m3) / (x. 0 ),m0) / (x. 4),m4 |= H <=> ((x. 4) '=' (x. 0 )) by A3, ZF_LANG1:80;
then ( M,((v / (x. 3),m3) / (x. 0 ),m0) / (x. 4),m4 |= H iff M,((v / (x. 3),m3) / (x. 0 ),m0) / (x. 4),m4 |= (x. 4) '=' (x. 0 ) ) by ZF_MODEL:19;
then A5: ( M,(v / (x. 3),m3) / (x. 0 ),m0 |= H iff (((v / (x. 3),m3) / (x. 0 ),m0) / (x. 4),m4) . (x. 4) = (((v / (x. 3),m3) / (x. 0 ),m0) / (x. 4),m4) . (x. 0 ) ) by A1, ZFMODEL2:10, ZF_MODEL:12;
( (((v / (x. 3),m3) / (x. 0 ),m0) / (x. 4),m4) . (x. 4) = m4 & ((v / (x. 3),m3) / (x. 0 ),m0) . (x. 0 ) = m0 ) by FUNCT_7:130;
hence ( M,(v / (x. 3),m3) / (x. 0 ),m0 |= H iff m4 = m0 ) by A2, A5, FUNCT_7:34; :: thesis: verum

end;

then A6: M,(v / (x. 3),m3) / (x. 0 ),m0 |= H ;
let m be Element of M; :: thesis: (def_func' H,v) .: m = {}
assume A7: (def_func' H,v) .: m <> {} ; :: thesis: contradiction
consider u being Element of (def_func' H,v) .: m;
consider u1 being set such that
A8: ( u1 in dom (def_func' H,v) & u1 in m & u = (def_func' H,v) . u1 ) by A7, FUNCT_1:def 12;
reconsider u1 = u1 as Element of M by A8;
( u1 = m0 & m = m0 ) by A4, A6;
hence contradiction by A8; :: thesis: verum