let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of I

for i being Element of I

for S being Subset of (A . i)

for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A holds product (L +* (i,S)) is Subset of (Segre_Product A)

let A be PLS-yielding ManySortedSet of I; :: thesis: for i being Element of I

for S being Subset of (A . i)

for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A holds product (L +* (i,S)) is Subset of (Segre_Product A)

let i be Element of I; :: thesis: for S being Subset of (A . i)

for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A holds product (L +* (i,S)) is Subset of (Segre_Product A)

let S be Subset of (A . i); :: thesis: for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A holds product (L +* (i,S)) is Subset of (Segre_Product A)

let L be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: product (L +* (i,S)) is Subset of (Segre_Product A)

A1: dom (L +* (i,S)) = I by PARTFUN1:def 2

.= dom (Carrier A) by PARTFUN1:def 2 ;

hence product (L +* (i,S)) is Subset of (Segre_Product A) by A1, A2, CARD_3:27; :: thesis: verum

for i being Element of I

for S being Subset of (A . i)

for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A holds product (L +* (i,S)) is Subset of (Segre_Product A)

let A be PLS-yielding ManySortedSet of I; :: thesis: for i being Element of I

for S being Subset of (A . i)

for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A holds product (L +* (i,S)) is Subset of (Segre_Product A)

let i be Element of I; :: thesis: for S being Subset of (A . i)

for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A holds product (L +* (i,S)) is Subset of (Segre_Product A)

let S be Subset of (A . i); :: thesis: for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A holds product (L +* (i,S)) is Subset of (Segre_Product A)

let L be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: product (L +* (i,S)) is Subset of (Segre_Product A)

A1: dom (L +* (i,S)) = I by PARTFUN1:def 2

.= dom (Carrier A) by PARTFUN1:def 2 ;

A2: now :: thesis: for a being object st a in dom (L +* (i,S)) holds

(L +* (i,S)) . a c= (Carrier A) . a

Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #)
by PENCIL_1:def 23;(L +* (i,S)) . a c= (Carrier A) . a

let a be object ; :: thesis: ( a in dom (L +* (i,S)) implies (L +* (i,S)) . b_{1} c= (Carrier A) . b_{1} )

assume a in dom (L +* (i,S)) ; :: thesis: (L +* (i,S)) . b_{1} c= (Carrier A) . b_{1}

then A3: a in I ;

then A4: a in dom L by PARTFUN1:def 2;

end;assume a in dom (L +* (i,S)) ; :: thesis: (L +* (i,S)) . b

then A3: a in I ;

then A4: a in dom L by PARTFUN1:def 2;

hence product (L +* (i,S)) is Subset of (Segre_Product A) by A1, A2, CARD_3:27; :: thesis: verum