let I be non empty set ; :: thesis: for i being Element of I
for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I
for p being Point of (Segre_Product A) ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( indx L = i & product L is Segre-Coset of A & p in product L )
let x be Element of I; :: thesis: for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I
for p being Point of (Segre_Product A) ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( indx L = x & product L is Segre-Coset of A & p in product L )
let A be TopStruct-yielding non-Trivial-yielding ManySortedSet of I; :: thesis: for p being Point of (Segre_Product A) ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( indx L = x & product L is Segre-Coset of A & p in product L )
let p0 be Point of (Segre_Product A); :: thesis: ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( indx L = x & product L is Segre-Coset of A & p0 in product L )
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 p09 = p0 as Element of Carrier A by Th6;
reconsider p = {p09} 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 & p0 in product b )
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 & p0 in product b )
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 {(p09 . i1)} by PZFMISC1:def 1;
then f . i1 = p09 . 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: p0 in product b
A12: dom p = I by PARTFUN1:def 2;

A13: now :: thesis: for z being object st z in I holds
p09 . z in (p +* (x,C)) . z

let z be object ; :: thesis: ( z in I implies p09 . b₁ in (p +* (x,C)) . b₁ )
assume A14: z in I ; :: thesis: p09 . b₁ in (p +* (x,C)) . b₁
then reconsider z1 = z as Element of I ;
dom A = I by PARTFUN1:def 2;
then A . z in rng A by A14, FUNCT_1:def 3;
then A . z is non trivial 1-sorted by PENCIL_1:def 18;
then reconsider tc = the carrier of (A . z1) as non trivial set ;
A15: not tc is empty ;

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

suppose A16: z = x ; :: thesis: p09 . b₁ in (p +* (x,C)) . b₁

p09 . z1 is Element of (Carrier A) . z1 by PBOOLE:def 14;
then p09 . z1 is Element of [#] (A . z1) by Th7;
then p09 . z1 in the carrier of (A . z1) by A15;
hence p09 . z in (p +* (x,C)) . z by A12, A16, FUNCT_7:31; :: thesis: verum

end;

suppose z <> x ; :: thesis: p09 . b₁ in (p +* (x,C)) . b₁

then (p +* (x,C)) . z = p . z by FUNCT_7:32;
then (p +* (x,C)) . z = {(p09 . z)} by A14, PZFMISC1:def 1;
hence p09 . z in (p +* (x,C)) . z by TARSKI:def 1; :: thesis: verum

end;

end;

end;

( dom p09 = I & dom (p +* (x,C)) = I ) by PARTFUN1:def 2;
hence p0 in product b by A13, CARD_3:9; :: thesis: verum