let I be non empty set ; :: thesis: for A being ManySortedSet of I
for i being Element of I
for S being non trivial set holds not A +* (i,S) is trivial-yielding
let A be ManySortedSet of I; :: thesis: for i being Element of I
for S being non trivial set holds not A +* (i,S) is trivial-yielding
let i be Element of I; :: thesis: for S being non trivial set holds not A +* (i,S) is trivial-yielding
let S be non trivial set ; :: thesis: not A +* (i,S) is trivial-yielding
take a = (A +* (i,S)) . i; :: according to PENCIL_1:def 16 :: thesis: ( a in rng (A +* (i,S)) & not a is trivial )
dom A = I by PARTFUN1:def 2;
then i in dom A ;
then i in dom (A +* (i,S)) by FUNCT_7:30;
hence a in rng (A +* (i,S)) by FUNCT_1:def 3; :: thesis: not a is trivial
dom A = I by PARTFUN1:def 2;
hence not a is trivial by FUNCT_7:31; :: thesis: verum