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 = {} )
consider m3 being Element of M;
assume that
A1: M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) and
A2: not x. 4 in Free H ; :: thesis: for m being Element of M holds (def_func' H,v) .: 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;
let m be Element of M; :: thesis: (def_func' H,v) .: m = {}
consider u being Element of (def_func' H,v) .: m;
assume (def_func' H,v) .: m <> {} ; :: thesis: contradiction
then consider u1 being set such that
A4: u1 in dom (def_func' H,v) and
A5: u1 in m and
u = (def_func' H,v) . u1 by FUNCT_1:def 12;
set f = (v / (x. 3),m3) / (x. 0 ),m0;
reconsider u1 = u1 as Element of M by A4;

A6: 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 A7: ( 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 A2, 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 A7, FUNCT_7:34, ZF_LANG1:86; :: thesis: verum

end;

then M,(v / (x. 3),m3) / (x. 0 ),m0 |= H ;
then ( u1 = m0 & m = m0 ) by A6;
hence contradiction by A5; :: thesis: verum