let M be non empty set ; :: thesis: id M is_definable_in M
take H = (x. 3) '=' (x. 4); :: according to ZFMODEL1:def 3 :: thesis: ( Free H c= {(x. 3),(x. 4)} & M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & id M = def_func (H,M) )
thus A1: Free H c= {(x. 3),(x. 4)} by ZF_LANG1:58; :: thesis: ( M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & id M = def_func (H,M) )
reconsider i = id M as Function of M,M ;

now :: thesis: for v being Function of VAR,M holds M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))))

let v be Function of VAR,M; :: thesis: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))))

now :: thesis: for m3 being Element of M holds M,v / ((x. 3),m3) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))

let m3 be Element of M; :: thesis: M,v / ((x. 3),m3) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))

now :: thesis: for m4 being Element of M holds M,((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4) |= H <=> ((x. 4) '=' (x. 0))

let m4 be Element of M; :: thesis: M,((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4) |= H <=> ((x. 4) '=' (x. 0))
A2: m3 = (v / ((x. 3),m3)) . (x. 3) by FUNCT_7:128;
A3: (((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4)) . (x. 0) = ((v / ((x. 3),m3)) / ((x. 0),m3)) . (x. 0) by FUNCT_7:32, ZF_LANG1:76;
A4: ((v / ((x. 3),m3)) / ((x. 0),m3)) . (x. 0) = m3 by FUNCT_7:128;
A5: ((v / ((x. 3),m3)) / ((x. 0),m3)) . (x. 3) = (v / ((x. 3),m3)) . (x. 3) by FUNCT_7:32, ZF_LANG1:76;
A6: (((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4)) . (x. 3) = ((v / ((x. 3),m3)) / ((x. 0),m3)) . (x. 3) by FUNCT_7:32, ZF_LANG1:76;

A7: now :: thesis: ( M,((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4) |= H implies M,((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) )

assume M,((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4) |= H ; :: thesis: M,((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4) |= (x. 4) '=' (x. 0)
then (((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4)) . (x. 3) = (((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4)) . (x. 4) by ZF_MODEL:12;
hence M,((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) by A6, A2, A5, A3, A4, ZF_MODEL:12; :: thesis: verum

end;

A8: (((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4)) . (x. 4) = m4 by FUNCT_7:128;

now :: thesis: ( M,((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) implies M,((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4) |= H )

assume M,((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) ; :: thesis: M,((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4) |= H
then m4 = m3 by A3, A4, A8, ZF_MODEL:12;
hence M,((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4) |= H by A6, A2, A5, A8, ZF_MODEL:12; :: thesis: verum

end;

hence M,((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4) |= H <=> ((x. 4) '=' (x. 0)) by A7, ZF_MODEL:19; :: thesis: verum

end;

then M,(v / ((x. 3),m3)) / ((x. 0),m3) |= All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) by ZF_LANG1:71;
hence M,v / ((x. 3),m3) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) by ZF_LANG1:73; :: thesis: verum

end;

hence M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) by ZF_LANG1:71; :: thesis: verum

end;

hence A9: M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ; :: thesis: id M = def_func (H,M)

now :: thesis: for a being Element of M holds i . a = (def_func (H,M)) . a

set v = the Function of VAR,M;
let a be Element of M; :: thesis: i . a = (def_func (H,M)) . a
A10: a = ( the Function of VAR,M / ((x. 3),a)) . (x. 3) by FUNCT_7:128;
A11: (( the Function of VAR,M / ((x. 3),a)) / ((x. 4),a)) . (x. 4) = a by FUNCT_7:128;
A12: (( the Function of VAR,M / ((x. 3),a)) / ((x. 4),a)) . (x. 3) = ( the Function of VAR,M / ((x. 3),a)) . (x. 3) by FUNCT_7:32, ZF_LANG1:76;
then M,( the Function of VAR,M / ((x. 3),a)) / ((x. 4),a) |= H by A10, A11, ZF_MODEL:12;
then (def_func (H,M)) . a = a by A1, A9, A12, A10, A11, ZFMODEL1:def 2;
hence i . a = (def_func (H,M)) . a ; :: thesis: verum

end;

hence id M = def_func (H,M) ; :: thesis: verum