let b be object ; :: thesis: ( b in f implies b in rng the mapping of ((a_net F) | i) )
assume A3: b in f ; :: thesis: b in rng the mapping of ((a_net F) | i)
then reconsider b = b as Element of L ;
reconsider f = f as Element of F by A1;
[b,f] in { [a,g] where a is Element of L, g is Element of F : a in g } by A3;
then reconsider k = [b,f] as Element of (a_net F) by YELLOW19:def 4;
reconsider l = k as Element of (a_net F) ;
[b,f] `1 = b ;
then A4: b = (a_net F) . k by YELLOW19:def 4;
k `2 c= i `2 by A2;
then i <= k by YELLOW19:def 4;
then l in { y where y is Element of (a_net F) : i <= y } ;
then reconsider k = k as Element of ((a_net F) | i) by WAYBEL_9:12;
reconsider k = k as Element of ((a_net F) | i) ;
(a_net F) . l = ((a_net F) | i) . k by WAYBEL_9:16;
then b in { (((a_net F) | i) . m) where m is Element of ((a_net F) | i) : verum } by A4;
hence b in rng the mapping of ((a_net F) | i) by WAYBEL11:19; :: thesis: verum

let b be object ; :: thesis: ( b in rng the mapping of ((a_net F) | i) implies b in f )
assume b in rng the mapping of ((a_net F) | i) ; :: thesis: b in f
then b in { (((a_net F) | i) . k) where k is Element of ((a_net F) | i) : verum } by WAYBEL11:19;
then consider k being Element of ((a_net F) | i) such that
A6: b = ((a_net F) | i) . k ;
A7: the carrier of ((a_net F) | i) c= the carrier of (a_net F) by WAYBEL_9:13;
then reconsider l = k as Element of (a_net F) ;
k in the carrier of (a_net F) by A7;
then A8: k in { [c,g] where c is Element of L, g is Element of F : c in g } by YELLOW19:def 4;
k in the carrier of ((a_net F) | i) ;
then k in { y where y is Element of (a_net F) : i <= y } by WAYBEL_9:12;
then ex y being Element of (a_net F) st
( k = y & i <= y ) ;
then A9: l `2 c= f by A2, YELLOW19:def 4;
consider c being Element of L, g being Element of F such that
A10: k = [c,g] and
A11: c in g by A8;
reconsider k = k as Element of ((a_net F) | i) ;
(a_net F) . l = ((a_net F) | i) . k by WAYBEL_9:16;
then b = l `1 by A6, YELLOW19:def 4;
hence b in f by A11, A9, A10; :: thesis: verum