let x be set ; :: thesis: for A being ManySortedSet of {x} holds A = x .--> (A . x)
let A be ManySortedSet of {x}; :: thesis: A = x .--> (A . x)
A1: dom A = {x} by PARTFUN1:def 2;
then rng A = {(A . x)} by FUNCT_1:4;
hence A = x .--> (A . x) by A1, FUNCOP_1:9; :: thesis: verum