let M be non empty set ; :: thesis: for H being ZF-formula
for v being Function of VAR ,M st not x. 0 in Free H & M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) holds
for m1, m2 being Element of M holds
( (def_func' H,v) . m1 = m2 iff M,(v / (x. 3),m1) / (x. 4),m2 |= H )
let H be ZF-formula; :: thesis: for v being Function of VAR ,M st not x. 0 in Free H & M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) holds
for m1, m2 being Element of M holds
( (def_func' H,v) . m1 = m2 iff M,(v / (x. 3),m1) / (x. 4),m2 |= H )
let v be Function of VAR ,M; :: thesis: ( not x. 0 in Free H & M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) implies for m1, m2 being Element of M holds
( (def_func' H,v) . m1 = m2 iff M,(v / (x. 3),m1) / (x. 4),m2 |= H ) )
assume A1: ( not x. 0 in Free H & M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) ) ; :: thesis: for m1, m2 being Element of M holds
( (def_func' H,v) . m1 = m2 iff M,(v / (x. 3),m1) / (x. 4),m2 |= H )
let m1, m2 be Element of M; :: thesis: ( (def_func' H,v) . m1 = m2 iff M,(v / (x. 3),m1) / (x. 4),m2 |= H )
x. 3 <> x. 4 by ZF_LANG1:86;
then A2: ( ((v / (x. 3),m1) / (x. 4),m2) . (x. 4) = m2 & (v / (x. 3),m1) . (x. 3) = m1 & ((v / (x. 3),m1) / (x. 4),m2) . (x. 3) = (v / (x. 3),m1) . (x. 3) ) by FUNCT_7:34, FUNCT_7:130;

now

let y be Variable; :: thesis: ( ((v / (x. 3),m1) / (x. 4),m2) . y <> v . y & x. 0 <> y & x. 3 <> y implies not x. 4 <> y )
assume A3: ((v / (x. 3),m1) / (x. 4),m2) . y <> v . y ; :: thesis: ( x. 0 <> y & x. 3 <> y implies not x. 4 <> y )
assume ( x. 0 <> y & x. 3 <> y & x. 4 <> y ) ; :: thesis: contradiction
then ( ((v / (x. 3),m1) / (x. 4),m2) . y = (v / (x. 3),m1) . y & (v / (x. 3),m1) . y = v . y ) by FUNCT_7:34;
hence contradiction by A3; :: thesis: verum

end;

hence ( (def_func' H,v) . m1 = m2 iff M,(v / (x. 3),m1) / (x. 4),m2 |= H ) by A1, A2, ZFMODEL1:def 1; :: thesis: verum