let I be non empty set ; :: thesis: for i being Element of I
for A being PLS-yielding ManySortedSet of I
for B being Block of (A . i)
for P being Element of Carrier A holds product ({P} +* (i,B)) is Block of ()

let i be Element of I; :: thesis: for A being PLS-yielding ManySortedSet of I
for B being Block of (A . i)
for P being Element of Carrier A holds product ({P} +* (i,B)) is Block of ()

let A be PLS-yielding ManySortedSet of I; :: thesis: for B being Block of (A . i)
for P being Element of Carrier A holds product ({P} +* (i,B)) is Block of ()

let B be Block of (A . i); :: thesis: for P being Element of Carrier A holds product ({P} +* (i,B)) is Block of ()
let P be Element of Carrier A; :: thesis: product ({P} +* (i,B)) is Block of ()
reconsider PP = {P} as ManySortedSubset of Carrier A by PENCIL_1:11;
B in the topology of (A . i) ;
then reconsider B1 = B as Subset of (A . i) ;
A1: now :: thesis: for j being Element of I st j <> i holds
({P} +* (i,B1)) . j is 1 -element
let j be Element of I; :: thesis: ( j <> i implies ({P} +* (i,B1)) . j is 1 -element )
assume j <> i ; :: thesis: ({P} +* (i,B1)) . j is 1 -element
then ({P} +* (i,B1)) . j = {P} . j by FUNCT_7:32;
hence ({P} +* (i,B1)) . j is 1 -element by Th15; :: thesis: verum
end;
2 c= card B by PENCIL_1:def 6;
then not B1 is trivial by PENCIL_1:4;
then reconsider S = PP +* (i,B1) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by ;
A2: now :: thesis: not indx S <> iend;
dom {P} = I by PARTFUN1:def 2;
then S . (indx S) = B1 by ;
hence product ({P} +* (i,B)) is Block of () by ; :: thesis: verum