let I be non empty set ; :: thesis: for M being ManySortedSet of I
for y being object holds
( y in rng M iff ex i being Element of I st y = M . i )
let M be ManySortedSet of I; :: thesis: for y being object holds
( y in rng M iff ex i being Element of I st y = M . i )
let y be object ; :: thesis: ( y in rng M iff ex i being Element of I st y = M . i )

hereby :: thesis: ( ex i being Element of I st y = M . i implies y in rng M )

assume y in rng M ; :: thesis: ex i being Element of I st y = M . i
then consider i0 being object such that
A1: ( i0 in dom M & y = M . i0 ) by FUNCT_1:def 3;
reconsider i = i0 as Element of I by A1;
take i = i; :: thesis: y = M . i
thus y = M . i by A1; :: thesis: verum

end;

given i being Element of I such that A2: y = M . i ; :: thesis: y in rng M
dom M = I by PARTFUN1:def 2;
hence y in rng M by A2, FUNCT_1:3; :: thesis: verum