let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of
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 ; :: 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: Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) by PENCIL_1:def 23;
A2: dom (L +* i,S) = I by PARTFUN1:def 4
.= dom (Carrier A) by PARTFUN1:def 4 ;

now

let a be set ; :: 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 by PARTFUN1:def 4;
then A4: a in dom L by PARTFUN1:def 4;

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:33;
then (L +* i,S) . a c= [#] (A . i) ;
hence (L +* i,S) . a c= (Carrier A) . a by A5, Th7; :: thesis: verum

end;

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

then A6: (L +* i,S) . a = L . a by FUNCT_7:34;
L c= Carrier A by PBOOLE:def 23;
hence (L +* i,S) . a c= (Carrier A) . a by A3, A6, PBOOLE:def 5; :: thesis: verum

end;

end;

end;

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