let S be non empty 1-sorted ; :: thesis: for N being net of S

for i being Element of N

for x being set holds

( x in rng the mapping of (N | i) iff ex j being Element of N st

( i <= j & x = N . j ) )

let N be net of S; :: thesis: for i being Element of N

for x being set holds

( x in rng the mapping of (N | i) iff ex j being Element of N st

( i <= j & x = N . j ) )

let i be Element of N; :: thesis: for x being set holds

( x in rng the mapping of (N | i) iff ex j being Element of N st

( i <= j & x = N . j ) )

let x be set ; :: thesis: ( x in rng the mapping of (N | i) iff ex j being Element of N st

( i <= j & x = N . j ) )

A1: dom the mapping of (N | i) = the carrier of (N | i) by FUNCT_2:def 1;

A7: x = N . j ; :: thesis: x in rng the mapping of (N | i)

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: verum

for i being Element of N

for x being set holds

( x in rng the mapping of (N | i) iff ex j being Element of N st

( i <= j & x = N . j ) )

let N be net of S; :: thesis: for i being Element of N

for x being set holds

( x in rng the mapping of (N | i) iff ex j being Element of N st

( i <= j & x = N . j ) )

let i be Element of N; :: thesis: for x being set holds

( x in rng the mapping of (N | i) iff ex j being Element of N st

( i <= j & x = N . j ) )

let x be set ; :: thesis: ( x in rng the mapping of (N | i) iff ex j being Element of N st

( i <= j & x = N . j ) )

A1: dom the mapping of (N | i) = the carrier of (N | i) by FUNCT_2:def 1;

hereby :: thesis: ( ex j being Element of N st

( i <= j & x = N . j ) implies x in rng the mapping of (N | i) )

given j being Element of N such that A6:
i <= j
and ( i <= j & x = N . j ) implies x in rng the mapping of (N | i) )

assume
x in rng the mapping of (N | i)
; :: thesis: ex j being Element of N st

( i <= j & x = N . j )

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: ( i <= j & x = N . j )

thus i <= j by A5; :: thesis: x = N . j

thus x = (N | i) . y by A3

.= N . j by A4, WAYBEL_9:16 ; :: thesis: verum

end;( i <= j & x = N . j )

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: ( i <= j & x = N . j )

thus i <= j by A5; :: thesis: x = N . j

thus x = (N | i) . y by A3

.= N . j by A4, WAYBEL_9:16 ; :: thesis: verum

A7: x = N . j ; :: thesis: x in rng the mapping of (N | i)

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: verum