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 ((FinSups f),L))

let J be set ; :: thesis: for f being Function of J, the carrier of L holds rng f c= rng (netmap ((FinSups f),L))

let f be Function of J, the carrier of L; :: thesis: rng f c= rng (netmap ((FinSups f),L))

for f being Function of J, the carrier of L holds rng f c= rng (netmap ((FinSups f),L))

let J be set ; :: thesis: for f being Function of J, the carrier of L holds rng f c= rng (netmap ((FinSups f),L))

let f be Function of J, the carrier of L; :: thesis: rng f c= rng (netmap ((FinSups f),L))

per cases
( not J is empty or J is empty )
;

end;

suppose A1:
not J is empty
; :: thesis: rng f c= rng (netmap ((FinSups f),L))

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng f or a in rng (netmap ((FinSups f),L)) )

assume a in rng f ; :: thesis: a in rng (netmap ((FinSups f),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 A2, FUNCT_1:def 3;

then reconsider fb = f . b as Element of L ;

A4: Im (f,b) = {fb} by A2, FUNCT_1:59;

{b} c= J by A1, ZFMISC_1:31;

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 A3, A4, YELLOW_0:39 ;

hence a in rng (netmap ((FinSups f),L)) by A5, A6, FUNCT_1:def 3; :: thesis: verum

end;assume a in rng f ; :: thesis: a in rng (netmap ((FinSups f),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 A2, FUNCT_1:def 3;

then reconsider fb = f . b as Element of L ;

A4: Im (f,b) = {fb} by A2, FUNCT_1:59;

{b} c= J by A1, ZFMISC_1:31;

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 A3, A4, YELLOW_0:39 ;

hence a in rng (netmap ((FinSups f),L)) by A5, A6, FUNCT_1:def 3; :: thesis: verum