let I be non empty set ; :: thesis: for i being Element of I
for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( indx L = i & product L is Segre-Coset of A )
let x be Element of I; :: thesis: for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( indx L = x & product L is Segre-Coset of A )
let A be TopStruct-yielding non-Trivial-yielding ManySortedSet of ; :: thesis: ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( indx L = x & product L is Segre-Coset of A )
dom A = I by PARTFUN1:def 4;
then A . x in rng A by FUNCT_1:12;
then not A . x is trivial by PENCIL_1:def 18;
then reconsider C = [#] (A . x) as non trivial set ;
consider p0 being Point of (Segre_Product A);
reconsider p0 = p0 as Element of Carrier A by Th6;
reconsider p = {p0} as ManySortedSubset of Carrier A by PENCIL_1:11;
reconsider b = p +* x,C as non trivial-yielding Segre-like ManySortedSubset of Carrier A by PENCIL_1:9, PENCIL_1:10, PENCIL_2:7;
take b ; :: thesis: ( indx b = x & product b is Segre-Coset of A )
dom p = I by PARTFUN1:def 4;
then A1: b . x = C by FUNCT_7:33;
hence A2: indx b = x by PENCIL_1:def 21; :: thesis: product b is Segre-Coset of A
product b c= the carrier of (Segre_Product A)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in product b or a in the carrier of (Segre_Product A) )
assume a in product b ; :: thesis: a in the carrier of (Segre_Product A)
then consider f being Function such that
A3: ( a = f & dom f = dom b & ( for x being set st x in dom b holds
f . x in b . x ) ) by CARD_3:def 5;
dom (Carrier A) = I by PARTFUN1:def 4;
then A4: dom f = dom (Carrier A) by A3, PARTFUN1:def 4;

A5: now

let i be set ; :: thesis: ( i in dom (Carrier A) implies f . b₁ in (Carrier A) . b₁ )
assume A6: i in dom (Carrier A) ; :: thesis: f . b₁ in (Carrier A) . b₁
then A7: f . i in b . i by A3, A4;
reconsider i1 = i as Element of I by A6, PARTFUN1:def 4;

per cases ( i1 = x or i1 <> x ) ;

suppose i1 = x ; :: thesis: f . b₁ in (Carrier A) . b₁

hence f . i in (Carrier A) . i by A1, A7, Th7; :: thesis: verum

end;

suppose i1 <> x ; :: thesis: f . b₁ in (Carrier A) . b₁

then f . i1 in p . i1 by A7, FUNCT_7:34;
then f . i1 in {(p0 . i1)} by PZFMISC1:def 1;
then f . i1 = p0 . i1 by TARSKI:def 1;
then A8: f . i1 is Element of (Carrier A) . i1 by PBOOLE:def 17;
I = dom A by PARTFUN1:def 4;
then A . i1 in rng A by FUNCT_1:12;
then not A . i1 is trivial by PENCIL_1:def 18;
then reconsider AA = the carrier of (A . i1) as non trivial set ;
not AA is empty ;
then not [#] (A . i1) is empty ;
then not (Carrier A) . i1 is empty by Th7;
hence f . i in (Carrier A) . i by A8; :: thesis: verum

end;

end;

end;

Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) by PENCIL_1:def 23;
hence a in the carrier of (Segre_Product A) by A3, A4, A5, CARD_3:def 5; :: thesis: verum

end;

hence product b is Segre-Coset of A by A1, A2, PENCIL_2:def 2; :: thesis: verum