let I be non empty set ; :: thesis: for i being Element of I
for A being 1-sorted-yielding non-Trivial-yielding ManySortedSet of I holds not A . i is trivial
let i be Element of I; :: thesis: for A being 1-sorted-yielding non-Trivial-yielding ManySortedSet of I holds not A . i is trivial
let A be 1-sorted-yielding non-Trivial-yielding ManySortedSet of I; :: thesis: not A . i is trivial
dom A = I by PARTFUN1:def 2;
then A . i in rng A by FUNCT_1:3;
hence not A . i is trivial by PENCIL_1:def 17; :: thesis: verum