let I be non empty set ; :: thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I holds rng (proj (J,i)) = the carrier of (J . i)
let J be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: for i being Element of I holds rng (proj (J,i)) = the carrier of (J . i)
let i be Element of I; :: thesis: rng (proj (J,i)) = the carrier of (J . i)
A1: dom (Carrier J) = I by PARTFUN1:def 2;
thus rng (proj (J,i)) = rng (proj ((Carrier J),i)) by WAYBEL18:def 4
.= (Carrier J) . i by A1, YELLOW17:3
.= [#] (J . i) by PENCIL_3:7
.= the carrier of (J . i) by STRUCT_0:def 3 ; :: thesis: verum