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