let I be set ; :: thesis: for M being ManySortedSet of I
for i being object st i in I holds
M . i is Component of M
let M be ManySortedSet of I; :: thesis: for i being object st i in I holds
M . i is Component of M
let i be object ; :: thesis: ( i in I implies M . i is Component of M )
assume A1: i in I ; :: thesis: M . i is Component of M
dom M = I by PARTFUN1:def 2;
hence M . i is Component of M by A1, FUNCT_1:def 3; :: thesis: verum