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

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