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:63; :: thesis: ( M |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) & id M = def_func H,M )

now

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

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

now

let m4 be Element of M; :: thesis: M,((v / (x. 3),m3) / (x. 0 ),m3) / (x. 4),m4 |= H <=> ((x. 4) '=' (x. 0 ))
A2: ( (((v / (x. 3),m3) / (x. 0 ),m3) / (x. 4),m4) . (x. 3) = ((v / (x. 3),m3) / (x. 0 ),m3) . (x. 3) & m3 = (v / (x. 3),m3) . (x. 3) & ((v / (x. 3),m3) / (x. 0 ),m3) . (x. 3) = (v / (x. 3),m3) . (x. 3) & (((v / (x. 3),m3) / (x. 0 ),m3) / (x. 4),m4) . (x. 0 ) = ((v / (x. 3),m3) / (x. 0 ),m3) . (x. 0 ) & ((v / (x. 3),m3) / (x. 0 ),m3) . (x. 0 ) = m3 & (((v / (x. 3),m3) / (x. 0 ),m3) / (x. 4),m4) . (x. 4) = m4 ) by Lm1, FUNCT_7:34, FUNCT_7:130;

A3: now

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 A2, ZF_MODEL:12; :: thesis: verum

end;

now

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 A2, ZF_MODEL:12;
hence M,((v / (x. 3),m3) / (x. 0 ),m3) / (x. 4),m4 |= H by A2, ZF_MODEL:12; :: thesis: verum

end;

hence M,((v / (x. 3),m3) / (x. 0 ),m3) / (x. 4),m4 |= H <=> ((x. 4) '=' (x. 0 )) by A3, 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:80;
hence M,v / (x. 3),m3 |= Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 )))) by ZF_LANG1:82; :: thesis: verum

end;

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

end;

hence A4: M |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) by ZF_MODEL:def 5; :: thesis: id M = def_func H,M
reconsider i = id M as Function of M,M ;

now

let a be Element of M; :: thesis: i . a = (def_func H,M) . a
consider v being Function of VAR ,M;
A5: ( ((v / (x. 3),a) / (x. 4),a) . (x. 3) = (v / (x. 3),a) . (x. 3) & a = (v / (x. 3),a) . (x. 3) & ((v / (x. 3),a) / (x. 4),a) . (x. 4) = a ) by Lm1, FUNCT_7:34, FUNCT_7:130;
then M,(v / (x. 3),a) / (x. 4),a |= H by ZF_MODEL:12;
then (def_func H,M) . a = a by A1, A4, A5, ZFMODEL1:def 2;
hence i . a = (def_func H,M) . a by FUNCT_1:35; :: thesis: verum

end;

hence id M = def_func H,M by FUNCT_2:113; :: thesis: verum