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

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