let I be non empty set ; :: thesis: for A being non-Empty TopStruct-yielding ManySortedSet of I

for p being Point of (Segre_Product A) holds p is Element of Carrier A

let A be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: for p being Point of (Segre_Product A) holds p is Element of Carrier A

let p be Point of (Segre_Product A); :: thesis: p is Element of Carrier A

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

then consider f being Function such that

A1: f = p and

A2: dom f = dom (Carrier A) and

A3: for x being object st x in dom (Carrier A) holds

f . x in (Carrier A) . x by CARD_3:def 5;

A4: dom f = I by A2, PARTFUN1:def 2;

then reconsider f = f as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

for i being object st i in I holds

f . i is Element of (Carrier A) . i by A2, A3, A4;

hence p is Element of Carrier A by A1, PBOOLE:def 14; :: thesis: verum

for p being Point of (Segre_Product A) holds p is Element of Carrier A

let A be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: for p being Point of (Segre_Product A) holds p is Element of Carrier A

let p be Point of (Segre_Product A); :: thesis: p is Element of Carrier A

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

then consider f being Function such that

A1: f = p and

A2: dom f = dom (Carrier A) and

A3: for x being object st x in dom (Carrier A) holds

f . x in (Carrier A) . x by CARD_3:def 5;

A4: dom f = I by A2, PARTFUN1:def 2;

then reconsider f = f as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

for i being object st i in I holds

f . i is Element of (Carrier A) . i by A2, A3, A4;

hence p is Element of Carrier A by A1, PBOOLE:def 14; :: thesis: verum