let I be set ; :: thesis: for A being ManySortedSet of holds (id A) .:.: A = A
let A be ManySortedSet of ; :: thesis: (id A) .:.: A = A
id A is "onto" by AUTALG_1:24;
then A1: rngs (id A) = A by EXTENS_1:13;
doms (id A) = A by MSSUBFAM:17;
hence (id A) .:.: A = A by A1, Th14; :: thesis: verum