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