let A be non empty AltGraph ; :: thesis: for o being Object of A holds (id A) . o = o
let o be Object of A; :: thesis: (id A) . o = o
A1: [o,o] in [: the carrier of A, the carrier of A:] by ZFMISC_1:87;
thus (id A) . o = ((id [: the carrier of A, the carrier of A:]) . [o,o]) `1 by Def29
.= [o,o] `1 by A1, FUNCT_1:18
.= o ; :: thesis: verum