let M be non empty set ; 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; 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; ( 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 that
A1:
not x. 0 in Free H
and
A2:
M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))))
; 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; ( (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 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 <> ylet y be
Variable;
( ((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
;
( 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
;
contradiction
((v / ((x. 3),m1)) / ((x. 4),m2)) . y = (v / ((x. 3),m1)) . y
by A7, FUNCT_7:32;
hence
contradiction
by A5, A6, FUNCT_7:32;
verum end;
A8:
((v / ((x. 3),m1)) / ((x. 4),m2)) . (x. 3) = (v / ((x. 3),m1)) . (x. 3)
by FUNCT_7:32, ZF_LANG1:76;
((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 A1, A2, A3, A8, A4, ZFMODEL1:def 1; verum