let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of I
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 I; :: 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 )

A1: now :: thesis: for j being Element of I st j <> indx L holds
(L +* (i,{p})) . j is 1 -element

let j be Element of I; :: thesis: ( j <> indx L implies (L +* (i,{p})) . b₁ is 1 -element )
A2: dom L = I by PARTFUN1:def 2;
assume A3: j <> indx L ; :: thesis: (L +* (i,{p})) . b₁ is 1 -element

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

suppose j = i ; :: thesis: (L +* (i,{p})) . b₁ is 1 -element

hence (L +* (i,{p})) . j is 1 -element by A2, FUNCT_7:31; :: thesis: verum

end;

suppose j <> i ; :: thesis: (L +* (i,{p})) . b₁ is 1 -element

then (L +* (i,{p})) . j = L . j by FUNCT_7:32;
hence (L +* (i,{p})) . j is 1 -element by A3, PENCIL_1:12; :: thesis: verum

end;

end;

end;

A4: L +* (i,{p}) c= Carrier A

proof

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

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

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

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

end;

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

A9: L c= Carrier A by PBOOLE:def 18;
(L +* (i,{p})) . a1 = L . a1 by A8, FUNCT_7:32;
hence (L +* (i,{p})) . a c= (Carrier A) . a by A9; :: thesis: verum

end;

end;

end;

assume i <> indx L ; :: thesis: L +* (i,{p}) is non trivial-yielding Segre-like ManySortedSubset of Carrier A
then (L +* (i,{p})) . (indx L) = L . (indx L) by FUNCT_7:32;
then A10: not (L +* (i,{p})) . (indx L) is trivial by PENCIL_1:def 21;
dom (L +* (i,{p})) = I by PARTFUN1:def 2;
then (L +* (i,{p})) . (indx L) in rng (L +* (i,{p})) by FUNCT_1:3;
hence L +* (i,{p}) is non trivial-yielding Segre-like ManySortedSubset of Carrier A by A4, A1, A10, PBOOLE:def 18, PENCIL_1:def 16, PENCIL_1:def 20; :: thesis: verum