let A be non empty AltCatStr ; :: thesis: for B being non empty SubCatStr of A
for o being object of B holds (incl B) . o = o
let B be non empty SubCatStr of A; :: thesis: for o being object of B holds (incl B) . o = o
let o be object of B; :: thesis: (incl B) . o = o
A1: [o,o] in [:the carrier of B,the carrier of B:] by ZFMISC_1:106;
thus (incl B) . o = ((id [:the carrier of B,the carrier of B:]) . [o,o]) `1 by Def29
.= [o,o] `1 by A1, FUNCT_1:35
.= o by MCART_1:7 ; :: thesis: verum