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

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