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

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

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

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 ()
let L be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: product (L +* (i,S)) is Subset of ()
A1: dom (L +* (i,S)) = I by PARTFUN1:def 2
.= dom () by PARTFUN1:def 2 ;
A2: now :: thesis: for a being object st a in dom (L +* (i,S)) holds
(L +* (i,S)) . a c= () . a
let a be object ; :: thesis: ( a in dom (L +* (i,S)) implies (L +* (i,S)) . b1 c= () . b1 )
assume a in dom (L +* (i,S)) ; :: thesis: (L +* (i,S)) . b1 c= () . b1
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)) . b1 c= () . b1
then (L +* (i,S)) . a = S by ;
then (L +* (i,S)) . a c= [#] (A . i) ;
hence (L +* (i,S)) . a c= () . a by ; :: thesis: verum
end;
suppose A6: a <> i ; :: thesis: (L +* (i,S)) . b1 c= () . b1
A7: L c= Carrier A by PBOOLE:def 18;
(L +* (i,S)) . a = L . a by ;
hence (L +* (i,S)) . a c= () . a by A3, A7; :: thesis: verum
end;
end;
end;
Segre_Product A = TopStruct(# (product ()),() #) by PENCIL_1:def 23;
hence product (L +* (i,S)) is Subset of () by ; :: thesis: verum