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