let L be non empty reflexive antisymmetric RelStr ; :: thesis: for J being set
for f being Function of J, the carrier of L holds rng f c= rng (netmap ((),L))

let J be set ; :: thesis: for f being Function of J, the carrier of L holds rng f c= rng (netmap ((),L))
let f be Function of J, the carrier of L; :: thesis: rng f c= rng (netmap ((),L))
per cases ( not J is empty or J is empty ) ;
suppose A1: not J is empty ; :: thesis: rng f c= rng (netmap ((),L))
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng f or a in rng (netmap ((),L)) )
assume a in rng f ; :: thesis: a in rng (netmap ((),L))
then consider b being object such that
A2: b in dom f and
A3: a = f . b by FUNCT_1:def 3;
reconsider b = b as Element of J by A2;
f . b in rng f by ;
then reconsider fb = f . b as Element of L ;
A4: Im (f,b) = {fb} by ;
{b} c= J by ;
then reconsider x = {b} as Element of Fin J by FINSUB_1:def 5;
consider g being Function of (Fin J), the carrier of L such that
A5: for x being Element of Fin J holds
( g . x = sup (f .: x) & FinSups f = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) by Def2;
dom g = Fin J by FUNCT_2:def 1;
then A6: x in dom g ;
g . {b} = sup (f .: x) by A5
.= a by ;
hence a in rng (netmap ((),L)) by ; :: thesis: verum
end;
suppose A7: J is empty ; :: thesis: rng f c= rng (netmap ((),L))
rng f = {} by A7;
hence rng f c= rng (netmap ((),L)) ; :: thesis: verum
end;
end;