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 )

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

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

A4:
L +* (i,{p}) c= Carrier A
(L +* (i,{p})) . j is 1 -element

let j be Element of I; :: thesis: ( j <> indx L implies (L +* (i,{p})) . b_{1} is 1 -element )

A2: dom L = I by PARTFUN1:def 2;

assume A3: j <> indx L ; :: thesis: (L +* (i,{p})) . b_{1} is 1 -element

end;A2: dom L = I by PARTFUN1:def 2;

assume A3: j <> indx L ; :: thesis: (L +* (i,{p})) . b

proof

assume
i <> indx L
; :: thesis: L +* (i,{p}) is non trivial-yielding Segre-like ManySortedSubset of Carrier A
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;

end;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;

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