let I be non empty set ; :: thesis: for i being Element of I
for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I 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 I 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 I; :: thesis: ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( indx L = x & product L is Segre-Coset of A )
set p0 = the Point of (Segre_Product A);
dom A = I by PARTFUN1:def 2;
then A . x in rng A by FUNCT_1:3;
then not A . x is trivial by PENCIL_1:def 18;
then reconsider C = [#] (A . x) as non trivial set ;
reconsider p0 = the Point of (Segre_Product A) 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 2;
then A1: b . x = C by FUNCT_7:31;
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 object ; :: 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 and
A4: dom f = dom b and
A5: for x being object st x in dom b holds
f . x in b . x by CARD_3:def 5;
dom (Carrier A) = I by PARTFUN1:def 2;
then A6: dom f = dom (Carrier A) by A4, PARTFUN1:def 2;

A7: now :: thesis: for i being object st i in dom (Carrier A) holds
f . i in (Carrier A) . i

let i be object ; :: thesis: ( i in dom (Carrier A) implies f . b₁ in (Carrier A) . b₁ )
assume A8: i in dom (Carrier A) ; :: thesis: f . b₁ in (Carrier A) . b₁
then reconsider i1 = i as Element of I ;
A9: f . i in b . i by A4, A5, A6, A8;

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, A9, Th7; :: thesis: verum

end;

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

I = dom A by PARTFUN1:def 2;
then A . i1 in rng A by FUNCT_1:3;
then not A . i1 is trivial by PENCIL_1:def 18;
then reconsider AA = the carrier of (A . i1) as non trivial set ;
f . i1 in p . i1 by A9, A10, FUNCT_7:32;
then f . i1 in {(p0 . i1)} by PZFMISC1:def 1;
then f . i1 = p0 . i1 by TARSKI:def 1;
then A11: f . i1 is Element of (Carrier A) . i1 by PBOOLE:def 14;
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 A11; :: 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, A6, A7, CARD_3:def 5; :: thesis: verum

end;

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