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 () 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 () 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 () 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 (); :: 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 ;
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 ()
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in product b or a in the carrier of () )
assume a in product b ; :: thesis: a in the carrier of ()
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 () = I by PARTFUN1:def 2;
then A6: dom f = dom () by ;
A7: now :: thesis: for i being object st i in dom () holds
f . i in () . i
let i be object ; :: thesis: ( i in dom () implies f . b1 in () . b1 )
assume A8: i in dom () ; :: thesis: f . b1 in () . b1
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 . b1 in () . b1
hence f . i in () . i by A1, A9, Th7; :: thesis: verum
end;
suppose A10: i1 <> x ; :: thesis: f . b1 in () . b1
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 ;
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 () . 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 () . i by A11; :: thesis: verum
end;
end;
end;
Segre_Product A = TopStruct(# (product ()),() #) by PENCIL_1:def 23;
hence a in the carrier of () by ; :: thesis: verum
end;
hence product b is Segre-Coset of A by ; :: 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 . b1 in (p +* (x,C)) . b1 )
assume A14: z in I ; :: thesis: p09 . b1 in (p +* (x,C)) . b1
then reconsider z1 = z as Element of I ;
dom A = I by PARTFUN1:def 2;
then A . z in rng A by ;
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 . b1 in (p +* (x,C)) . b1
p09 . z1 is Element of () . 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 ; :: thesis: verum
end;
suppose z <> x ; :: thesis: p09 . b1 in (p +* (x,C)) . b1
then (p +* (x,C)) . z = p . z by FUNCT_7:32;
then (p +* (x,C)) . z = {(p09 . z)} by ;
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 ; :: thesis: verum