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:106;
thus (id A) . o = ((id [: the carrier of A, the carrier of A:]) . [o,o]) `1 by Def30
.= [o,o] `1 by A1, FUNCT_1:35
.= o by MCART_1:7 ; :: thesis: verum