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 ;

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

let a be object ; :: thesis: ( a in dom (L +* (i,S)) implies (L +* (i,S)) . b₁ c= (Carrier A) . b₁ )
assume a in dom (L +* (i,S)) ; :: thesis: (L +* (i,S)) . b₁ c= (Carrier A) . b₁
then A3: a in I ;
then A4: a in dom L by PARTFUN1:def 2;

per cases ( a = i or a <> i ) ;

suppose A5: a = i ; :: thesis: (L +* (i,S)) . b₁ c= (Carrier A) . b₁

then (L +* (i,S)) . a = S by A4, FUNCT_7:31;
then (L +* (i,S)) . a c= [#] (A . i) ;
hence (L +* (i,S)) . a c= (Carrier A) . a by A5, Th7; :: thesis: verum

end;

suppose A6: a <> i ; :: thesis: (L +* (i,S)) . b₁ c= (Carrier A) . b₁

A7: L c= Carrier A by PBOOLE:def 18;
(L +* (i,S)) . a = L . a by A6, FUNCT_7:32;
hence (L +* (i,S)) . a c= (Carrier A) . a by A3, A7; :: thesis: verum

end;

end;

end;

Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) by PENCIL_1:def 23;
hence product (L +* (i,S)) is Subset of (Segre_Product A) by A1, A2, CARD_3:27; :: thesis: verum