let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of
for i being Element of I
for p being Point of (A . i)
for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st i <> indx L holds
L +* i,{p} is non trivial-yielding Segre-like ManySortedSubset of Carrier A
let A be PLS-yielding ManySortedSet of ; :: thesis: for i being Element of I
for p being Point of (A . i)
for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st i <> indx L holds
L +* i,{p} is non trivial-yielding Segre-like ManySortedSubset of Carrier A
let i be Element of I; :: thesis: for p being Point of (A . i)
for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st i <> indx L holds
L +* i,{p} is non trivial-yielding Segre-like ManySortedSubset of Carrier A
let p be Point of (A . i); :: thesis: for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st i <> indx L holds
L +* i,{p} is non trivial-yielding Segre-like ManySortedSubset of Carrier A
let L be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( i <> indx L implies L +* i,{p} is non trivial-yielding Segre-like ManySortedSubset of Carrier A )
assume A1: i <> indx L ; :: thesis: L +* i,{p} is non trivial-yielding Segre-like ManySortedSubset of Carrier A
A2: L +* i,{p} c= Carrier A

proof

let a be set ; :: according to PBOOLE:def 5 :: thesis: ( not a in I or (L +* i,{p}) . a c= (Carrier A) . a )
assume A3: a in I ; :: thesis: (L +* i,{p}) . a c= (Carrier A) . a
then reconsider a1 = a as Element of I ;
A4: a1 in dom L by A3, PARTFUN1:def 4;

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

suppose A5: a = i ; :: thesis: (L +* i,{p}) . a c= (Carrier A) . a

then (L +* i,{p}) . a1 = {p} by A4, FUNCT_7:33;
then (L +* i,{p}) . a1 c= [#] (A . a1) by A5;
hence (L +* i,{p}) . a c= (Carrier A) . a by Th7; :: thesis: verum

end;

suppose a <> i ; :: thesis: (L +* i,{p}) . a c= (Carrier A) . a

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

end;

end;

end;

A7: now

let j be Element of I; :: thesis: ( j <> indx L implies ( not (L +* i,{p}) . b₁ is empty & (L +* i,{p}) . b₁ is trivial ) )
A8: dom L = I by PARTFUN1:def 4;
assume A9: j <> indx L ; :: thesis: ( not (L +* i,{p}) . b₁ is empty & (L +* i,{p}) . b₁ is trivial )

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

suppose j = i ; :: thesis: ( not (L +* i,{p}) . b₁ is empty & (L +* i,{p}) . b₁ is trivial )

hence ( not (L +* i,{p}) . j is empty & (L +* i,{p}) . j is trivial ) by A8, FUNCT_7:33; :: thesis: verum

end;

suppose j <> i ; :: thesis: ( not (L +* i,{p}) . b₁ is empty & (L +* i,{p}) . b₁ is trivial )

then (L +* i,{p}) . j = L . j by FUNCT_7:34;
hence ( not (L +* i,{p}) . j is empty & (L +* i,{p}) . j is trivial ) by A9, PENCIL_1:12; :: thesis: verum

end;

end;

end;

dom (L +* i,{p}) = I by PARTFUN1:def 4;
then A10: (L +* i,{p}) . (indx L) in rng (L +* i,{p}) by FUNCT_1:12;
(L +* i,{p}) . (indx L) = L . (indx L) by A1, FUNCT_7:34;
then not (L +* i,{p}) . (indx L) is trivial by PENCIL_1:def 21;
hence L +* i,{p} is non trivial-yielding Segre-like ManySortedSubset of Carrier A by A2, A7, A10, PBOOLE:def 23, PENCIL_1:def 16, PENCIL_1:def 20; :: thesis: verum