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

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