let I be non empty set ; :: thesis: for P being ManySortedSet of I
for i being Element of I holds {P} . i is 1 -element
let P be ManySortedSet of I; :: thesis: for i being Element of I holds {P} . i is 1 -element
let i be Element of I; :: thesis: {P} . i is 1 -element
{P} . i = {(P . i)} by PZFMISC1:def 1;
hence {P} . i is 1 -element ; :: thesis: verum