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)

A12: dom p = I by PARTFUN1:def 2;

hence p0 in product b by A13, CARD_3:9; :: thesis: verum

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

hence
product b is Segre-Coset of A
by A1, A2, PENCIL_2:def 2; :: thesis: p0 in product b
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;

hence a in the carrier of (Segre_Product A) by A3, A6, A7, CARD_3:def 5; :: thesis: verum

end;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

Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #)
by PENCIL_1:def 23;f . i in (Carrier A) . i

let i be object ; :: thesis: ( i in dom (Carrier A) implies f . b_{1} in (Carrier A) . b_{1} )

assume A8: i in dom (Carrier A) ; :: thesis: f . b_{1} in (Carrier A) . b_{1}

then reconsider i1 = i as Element of I ;

A9: f . i in b . i by A4, A5, A6, A8;

end;assume A8: i in dom (Carrier A) ; :: thesis: f . 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 )
;

end;

suppose A10:
i1 <> x
; :: thesis: f . b_{1} in (Carrier A) . b_{1}

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;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

hence a in the carrier of (Segre_Product A) by A3, A6, A7, CARD_3:def 5; :: thesis: verum

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

( dom p09 = I & dom (p +* (x,C)) = I )
by PARTFUN1:def 2;p09 . z in (p +* (x,C)) . z

let z be object ; :: thesis: ( z in I implies p09 . b_{1} in (p +* (x,C)) . b_{1} )

assume A14: z in I ; :: thesis: p09 . b_{1} in (p +* (x,C)) . b_{1}

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 ;

end;assume A14: z in I ; :: thesis: p09 . 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 )
;

end;

suppose A16:
z = x
; :: thesis: p09 . b_{1} in (p +* (x,C)) . b_{1}

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;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

hence p0 in product b by A13, CARD_3:9; :: thesis: verum