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

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