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 4;
then rng A = {(A . x)} by FUNCT_1:14;
hence A = x .--> (A . x) by A1, FUNCOP_1:15; :: thesis: verum