let M be non empty set ; :: thesis: for H being ZF-formula
for v being Function of VAR ,M st Free H c= {(x. 3),(x. 4)} & M |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) holds
def_func' H,v = def_func H,M
let H be ZF-formula; :: thesis: for v being Function of VAR ,M st Free H c= {(x. 3),(x. 4)} & M |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) holds
def_func' H,v = def_func H,M
let v be Function of VAR ,M; :: thesis: ( Free H c= {(x. 3),(x. 4)} & M |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) implies def_func' H,v = def_func H,M )
assume that
A1: Free H c= {(x. 3),(x. 4)} and
A2: M |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) ; :: thesis: def_func' H,v = def_func H,M
A3: M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) by A2, ZF_MODEL:def 5;
let a be Element of M; :: according to FUNCT_2:def 9 :: thesis: (def_func' H,v) . a = (def_func H,M) . a
set r = (def_func' H,v) . a;
A4: ((v / (x. 3),a) / (x. 4),((def_func' H,v) . a)) . (x. 3) = (v / (x. 3),a) . (x. 3) by FUNCT_7:34, ZF_LANG1:86;
not x. 0 in Free H by A1, Lm1, Lm2, TARSKI:def 2;
then A5: M,(v / (x. 3),a) / (x. 4),((def_func' H,v) . a) |= H by A3, Th11;
A6: (v / (x. 3),a) . (x. 3) = a by FUNCT_7:130;
((v / (x. 3),a) / (x. 4),((def_func' H,v) . a)) . (x. 4) = (def_func' H,v) . a by FUNCT_7:130;
hence (def_func' H,v) . a = (def_func H,M) . a by A1, A2, A5, A4, A6, ZFMODEL1:def 2; :: thesis: verum