let X be set ; :: thesis: for C being Element of CSp X holds
( (id$ C) `2 = id (union C) & dom (id$ C) = C & cod (id$ C) = C )
let C be Element of CSp X; :: thesis: ( (id$ C) `2 = id (union C) & dom (id$ C) = C & cod (id$ C) = C )
[[(dom (id$ C)),(cod (id$ C))],((id$ C) `2 )] = [[C,C],(id (union C))] by Th20;
hence ( (id$ C) `2 = id (union C) & dom (id$ C) = C & cod (id$ C) = C ) by Lm2, ZFMISC_1:33; :: thesis: verum