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;
let a be Element of M; :: according to FUNCT_2:def 8 :: 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:32, ZF_LANG1:76;
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, Th10;
A6: (v / ((x. 3),a)) . (x. 3) = a by FUNCT_7:128;
((v / ((x. 3),a)) / ((x. 4),((def_func' (H,v)) . a))) . (x. 4) = (def_func' (H,v)) . a by FUNCT_7:128;
hence (def_func' (H,v)) . a = (def_func (H,M)) . a by A1, A2, A5, A4, A6, ZFMODEL1:def 2; :: thesis: verum