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 (Segre_Product A)

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 (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)) ;

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;

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; :: thesis: verum

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; :: 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 :: thesis: for i being Element of I st i <> indx L holds

(L +* ((indx L),B1)) . i is 1 -element

2 c= card B
by PENCIL_1:def 6;(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 A2, PENCIL_1:12; :: thesis: verum

end;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 A2, PENCIL_1:12; :: thesis: verum

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 :: thesis: not indx S <> indx L

dom L = I
by PARTFUN1:def 2;assume
indx S <> indx L
; :: thesis: contradiction

then S . (indx S) is 1 -element by A1;

hence contradiction by PENCIL_1:def 21; :: thesis: verum

end;then S . (indx S) is 1 -element by A1;

hence contradiction by PENCIL_1:def 21; :: thesis: verum

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; :: thesis: verum