let I be non empty set ; :: thesis: for A being non-Empty TopStruct-yielding ManySortedSet of I
for x being Point of (Segre_Product A) holds x is ManySortedSet of I
let A be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: for x being Point of (Segre_Product A) holds x is ManySortedSet of I
let x be Point of (Segre_Product A); :: thesis: x is ManySortedSet of I
consider f being Function such that
A1: x = f and
A2: dom f = dom (Carrier A) and
for a being set st a in dom (Carrier A) holds
f . a in (Carrier A) . a by CARD_3:def 5;
dom f = I by A2, PARTFUN1:def 4;
hence x is ManySortedSet of I by A1, PARTFUN1:def 4, RELAT_1:def 18; :: thesis: verum