consider L being non trivial-yielding Segre-like ManySortedSubset of Carrier A;
reconsider C = L +* (indx L),([#] (A . (indx L))) as ManySortedSubset of Carrier A by Th7;
dom A = I by PARTFUN1:def 4;
then A . (indx L) in rng A by FUNCT_1:12;
then not A . (indx L) is trivial by PENCIL_1:def 17;
then A1: not the carrier of (A . (indx L)) is trivial ;
then reconsider C = C as non trivial-yielding Segre-like ManySortedSubset of Carrier A by PENCIL_1:27;
A2: ( dom C = I & dom (Carrier A) = I ) by PARTFUN1:def 4;
C c= Carrier A by PBOOLE:def 23;
then for a being set st a in I holds
C . a c= (Carrier A) . a by PBOOLE:def 5;
then reconsider P = product C as Subset of (Segre_Product A) by A2, CARD_3:38;
take P ; :: thesis: ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( P = product L & L . (indx L) = [#] (A . (indx L)) )
dom L = I by PARTFUN1:def 4;
then A3: C . (indx L) = [#] (A . (indx L)) by FUNCT_7:33;
then indx C = indx L by A1, PENCIL_1:def 21;
hence ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( P = product L & L . (indx L) = [#] (A . (indx L)) ) by A3; :: thesis: verum