let S be non empty 1-sorted ; :: thesis:
let N be net of S; :: thesis:
let i be Element of N; :: thesis:
let x be set ; :: thesis:
A1: dom the mapping of (N | i) = the carrier of (N | i) by FUNCT_2:def 1;

hereby :: thesis:

assume x in rng the mapping of (N | i) ; :: thesis:
then consider y being object such that
A2: y in the carrier of (N | i) and
A3: x = the mapping of (N | i) . y by A1, FUNCT_1:def 3;
reconsider y = y as Element of (N | i) by A2;
consider j being Element of N such that
A4: j = y and
A5: i <= j by WAYBEL_9:def 7;
take j = j; :: thesis:
thus i <= j by A5; :: thesis:
thus x = (N | i) . y by A3
.= N . j by A4, WAYBEL_9:16 ; :: thesis:

end;

given j being Element of N such that A6: i <= j and
A7: x = N . j ; :: thesis:
reconsider k = j as Element of (N | i) by A6, WAYBEL_9:def 7;
A8: x = (N | i) . k by A7, WAYBEL_9:16
.= the mapping of (N | i) . j ;
j in the carrier of (N | i) by A6, WAYBEL_9:def 7;
hence x in rng the mapping of (N | i) by A1, A8, FUNCT_1:def 3; :: thesis: