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
A1: rngs (id A) = A by EXTENS_1:9;
doms (id A) = A by MSSUBFAM:17;
hence (id A) .:.: A = A by A1, Th13; :: thesis: verum