let L be non empty reflexive antisymmetric RelStr ; 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 ; 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; rng f c= rng (netmap ((FinSups f),L))
per cases
( not J is empty or J is empty )
;
suppose A1:
not
J is
empty
;
rng f c= rng (netmap ((FinSups f),L))let a be
object ;
TARSKI:def 3 ( not a in rng f or a in rng (netmap ((FinSups f),L)) )assume
a in rng f
;
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;
verum end;