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 & dom f = dom (Carrier A) & ( for x being set st x in dom (Carrier A) holds
f . x in (Carrier A) . x ) ) by CARD_3:def 5;
A2: dom f = I by A1, PBOOLE:def 3;
then reconsider f = f as ManySortedSet of I by PBOOLE:def 3;
for i being set st i in I holds
f . i is Element of (Carrier A) . i by A1, A2;
hence p is Element of Carrier A by A1, PBOOLE:def 17; :: thesis: verum