let I be non empty set ; :: thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for f being Element of (product J) holds (proj (J,i)) . f = f . i
let J be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: for i being Element of I
for f being Element of (product J) holds (proj (J,i)) . f = f . i
let i be Element of I; :: thesis: for f being Element of (product J) holds (proj (J,i)) . f = f . i
let f be Element of (product J); :: thesis: (proj (J,i)) . f = f . i
f in the carrier of (product J) ;
then f in product (Carrier J) by WAYBEL18:def 3;
then f in dom (proj ((Carrier J),i)) by CARD_3:def 16;
then (proj ((Carrier J),i)) . f = f . i by CARD_3:def 16;
hence (proj (J,i)) . f = f . i by WAYBEL18:def 4; :: thesis: verum