let I, Y be non empty set ; :: thesis: for M being Y -valued ManySortedSet of I
for x being Element of I holds M . x = M /. x
let M be Y -valued ManySortedSet of I; :: thesis: for x being Element of I holds M . x = M /. x
let x be Element of I; :: thesis: M . x = M /. x
dom M = I by PARTFUN1:def 2;
hence M . x = M /. x by PARTFUN1:def 6; :: thesis: verum