let I be non empty set ; 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 (Segre_Product A)
let A be 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 (Segre_Product A)
let L be 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 (Segre_Product A)
let B be Block of (A . (indx L)); product (L +* ((indx L),B)) is Block of (Segre_Product A)
B in the topology of (A . (indx L))
;
then reconsider B1 = B as Subset of (A . (indx L)) ;
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 A1, PENCIL_1:9, PENCIL_1:def 20, PENCIL_2:7;
dom L = I
by PARTFUN1:def 2;
then
S . (indx S) = B1
by A3, FUNCT_7:31;
hence
product (L +* ((indx L),B)) is Block of (Segre_Product A)
by A3, PENCIL_1:24; verum