let I be non empty set ; :: thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I holds (proj (J,i)) " ([#] (J . i)) = [#] (product J)
let J be non-Empty TopStruct-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 2;
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:2;
hence (proj (J,i)) " ([#] (J . i)) = [#] (product J) by WAYBEL18:def 4; :: thesis: verum