set L = the non trivial-yielding Segre-like ManySortedSubset of Carrier A;
reconsider C = the non trivial-yielding Segre-like ManySortedSubset of Carrier A +* ((indx the non trivial-yielding Segre-like ManySortedSubset of Carrier A),([#] (A . (indx the non trivial-yielding Segre-like ManySortedSubset of Carrier A)))) as ManySortedSubset of Carrier A by Th7;
A1: dom (Carrier A) = I by PARTFUN1:def 2;
dom A = I by PARTFUN1:def 2;
then A . (indx the non trivial-yielding Segre-like ManySortedSubset of Carrier A) in rng A by FUNCT_1:3;
then A2: not A . (indx the non trivial-yielding Segre-like ManySortedSubset of Carrier A) 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 18;
then A3: for a being object st a in I holds
C . a c= (Carrier A) . a ;
dom C = I by PARTFUN1:def 2;
then reconsider P = product C as Subset of (Segre_Product A) by A1, A3, CARD_3:27;
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 the non trivial-yielding Segre-like ManySortedSubset of Carrier A = I by PARTFUN1:def 2;
then A4: C . (indx the non trivial-yielding Segre-like ManySortedSubset of Carrier A) = [#] (A . (indx the non trivial-yielding Segre-like ManySortedSubset of Carrier A)) by FUNCT_7:31;
then indx C = indx the non trivial-yielding Segre-like ManySortedSubset of Carrier A 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