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

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