let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I holds (proj J,i) " ([#] (J . i)) = [#] (product J)
let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for i being Element of I holds (proj J,i) " ([#] (J . i)) = [#] (product J)
let i be Element of I; :: thesis: (proj J,i) " ([#] (J . i)) = [#] (product J)
i in I ;
then i in dom (Carrier J) by PARTFUN1:def 4;
then (proj (Carrier J),i) " ((Carrier J) . i) = product (Carrier J) by Th4;
then (proj (Carrier J),i) " ((Carrier J) . i) = [#] (product J) by WAYBEL18:def 3;
then (proj (Carrier J),i) " ([#] (J . i)) = [#] (product J) by YELLOW_6:9;
hence (proj J,i) " ([#] (J . i)) = [#] (product J) by WAYBEL18:def 4; :: thesis: verum