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

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