let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of
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 ; :: 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 (Segre_Product A)
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 (Segre_Product A)
let B be Block of (A . (indx L)); :: thesis: 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)) ;

A1: now

let i be Element of I; :: thesis: ( i <> indx L implies ( not (L +* (indx L),B1) . i is empty & (L +* (indx L),B1) . i is trivial ) )
assume A2: i <> indx L ; :: thesis: ( not (L +* (indx L),B1) . i is empty & (L +* (indx L),B1) . i is trivial )
then (L +* (indx L),B1) . i = L . i by FUNCT_7:34;
hence ( not (L +* (indx L),B1) . i is empty & (L +* (indx L),B1) . i is trivial ) by A2, PENCIL_1:12; :: 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 A1, PENCIL_1:9, PENCIL_1:def 20, PENCIL_2:7;

A3: now

assume indx S <> indx L ; :: thesis: contradiction
then ( not S . (indx S) is empty & S . (indx S) is trivial ) by A1;
hence contradiction by PENCIL_1:def 21; :: thesis: verum

end;

dom L = I by PARTFUN1:def 4;
then S . (indx S) = B1 by A3, FUNCT_7:33;
hence product (L +* (indx L),B) is Block of (Segre_Product A) by A3, PENCIL_1:24; :: thesis: verum