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)
per cases
( not J is empty or J is empty )
;
suppose A1:
not
J is
empty
;
:: thesis: rng f c= rng (netmap (FinSups f),L)let a be
set ;
:: 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
set such that A2:
(
b in dom f &
a = f . b )
by FUNCT_1:def 5;
consider g being
Function of
(Fin J),the
carrier of
L such that A3:
for
x being
Element of
Fin J holds
(
g . x = sup (f .: x) &
FinSups f = NetStr(#
(Fin J),
(RelIncl (Fin J)),
g #) )
by Def2;
reconsider b =
b as
Element of
J by A2;
{b} c= J
by A1, ZFMISC_1:37;
then reconsider x =
{b} as
Element of
Fin J by FINSUB_1:def 5;
dom g = Fin J
by FUNCT_2:def 1;
then A4:
x in dom g
;
f . b in rng f
by A2, FUNCT_1:def 5;
then reconsider fb =
f . b as
Element of
L ;
A5:
Im f,
b = {fb}
by A2, FUNCT_1:117;
g . {b} =
sup (f .: x)
by A3
.=
a
by A2, A5, YELLOW_0:39
;
hence
a in rng (netmap (FinSups f),L)
by A3, A4, FUNCT_1:def 5;
:: thesis: verum end;