let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of I
for x being set holds
( x is Block of (Segre_Product A) iff ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) ) )
let A be PLS-yielding ManySortedSet of I; :: thesis: for x being set holds
( x is Block of (Segre_Product A) iff ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) ) )
let x be set ; :: thesis: ( x is Block of (Segre_Product A) iff ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) ) )
thus ( x is Block of (Segre_Product A) implies ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) ) ) :: thesis: ( ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) ) implies x is Block of (Segre_Product A) )

proof

assume A1: x is Block of (Segre_Product A) ; :: thesis: ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) )
then consider L being Segre-like ManySortedSubset of Carrier A such that
A2: x = product L and
A3: ex i being Element of I st L . i is Block of (A . i) by Def22;
2 c= card (product L) by A1, A2, Def6;
then reconsider L = L as non trivial-yielding Segre-like ManySortedSubset of Carrier A by Th13;
consider i being Element of I such that
A4: L . i is Block of (A . i) by A3;

now :: thesis: not i <> indx L

assume i <> indx L ; :: thesis: contradiction
then A5: L . i is 1 -element by Th12;
2 c= card (L . i) by A4, Def6;
hence contradiction by A5, Th4; :: thesis: verum

end;

hence ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) ) by A2, A4; :: thesis: verum

end;

given L being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A6: ( x = product L & L . (indx L) is Block of (A . (indx L)) ) ; :: thesis: x is Block of (Segre_Product A)
thus x is Block of (Segre_Product A) by A6, Def22; :: thesis: verum