let I be non empty set ; :: thesis: for M being ManySortedSet of I
for A being Component of M ex i being object st
( i in I & A = M . i )
let M be ManySortedSet of I; :: thesis: for A being Component of M ex i being object st
( i in I & A = M . i )
let A be Component of M; :: thesis: ex i being object st
( i in I & A = M . i )
A1: dom M = I by PARTFUN1:def 2;
then rng M <> {} by RELAT_1:42;
hence ex i being object st
( i in I & A = M . i ) by A1, FUNCT_1:def 3; :: thesis: verum