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 ((),(All ((x. 4),(H <=> ((x. 4) '=' ()))))))) 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 ((),(All ((x. 4),(H <=> ((x. 4) '=' ()))))))) 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 ((),(All ((x. 4),(H <=> ((x. 4) '=' ()))))))) 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 that
A1: not x. 0 in Free H and
A2: M,v |= All ((x. 3),(Ex ((),(All ((x. 4),(H <=> ((x. 4) '=' ()))))))) ; :: 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 )
A3: (v / ((x. 3),m1)) . (x. 3) = m1 by FUNCT_7:128;
A4: now :: thesis: for y being Variable st ((v / ((x. 3),m1)) / ((x. 4),m2)) . y <> v . y & x. 0 <> y & x. 3 <> y holds
not x. 4 <> y
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 A5: ((v / ((x. 3),m1)) / ((x. 4),m2)) . y <> v . y ; :: thesis: ( x. 0 <> y & x. 3 <> y implies not x. 4 <> y )
assume that
x. 0 <> y and
A6: x. 3 <> y and
A7: x. 4 <> y ; :: thesis: contradiction
((v / ((x. 3),m1)) / ((x. 4),m2)) . y = (v / ((x. 3),m1)) . y by ;
hence contradiction by A5, A6, FUNCT_7:32; :: thesis: verum
end;
A8: ((v / ((x. 3),m1)) / ((x. 4),m2)) . (x. 3) = (v / ((x. 3),m1)) . (x. 3) by ;
((v / ((x. 3),m1)) / ((x. 4),m2)) . (x. 4) = m2 by FUNCT_7:128;
hence ( (def_func' (H,v)) . m1 = m2 iff M,(v / ((x. 3),m1)) / ((x. 4),m2) |= H ) by ; :: thesis: verum