let I be non empty set ; :: thesis: for A being ManySortedSet of
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 ; :: 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 4;
then i in dom A ;
then i in dom (A +* i,S) by FUNCT_7:32;
hence a in rng (A +* i,S) by FUNCT_1:def 5; :: thesis: not a is trivial
dom A = I by PARTFUN1:def 4;
hence not a is trivial by FUNCT_7:33; :: thesis: verum