let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of I
for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A
for B being Block of (A . (indx L)) holds product (L +* ((indx L),B)) is Block of ()

let A be PLS-yielding ManySortedSet of I; :: thesis: for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A
for B being Block of (A . (indx L)) holds product (L +* ((indx L),B)) is Block of ()

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