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;
A1: dom (Carrier A) = I by PARTFUN1:def 4;
dom A = I by PARTFUN1:def 4;
then A . (indx L) in rng A by FUNCT_1:12;
then A2: not A . (indx L) is trivial by PENCIL_1:def 17;
then reconsider C = C as non trivial-yielding Segre-like ManySortedSubset of Carrier A by PENCIL_1:27;
C c= Carrier A by PBOOLE:def 23;
then A3: for a being set st a in I holds
C . a c= (Carrier A) . a by PBOOLE:def 5;
dom C = I by PARTFUN1:def 4;
then reconsider P = product C as Subset of (Segre_Product A) by A1, A3, 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 A4: C . (indx L) = [#] (A . (indx L)) by FUNCT_7:33;
then indx C = indx L by A2, 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 A4; :: thesis: verum