let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of
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 TopSpace-yielding ManySortedSet of ; :: 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 PRALG_3:def 2;
then (proj (Carrier J),i) . f = f . i by PRALG_3:def 2;
hence (proj J,i) . f = f . i by WAYBEL18:def 4; :: thesis: verum