let L be non empty RelStr ; :: thesis: for J being set

for f being Function of J, the carrier of L st ( for x being set holds ex_sup_of f .: x,L ) holds

rng (netmap ((FinSups f),L)) c= finsups (rng f)

let J be set ; :: thesis: for f being Function of J, the carrier of L st ( for x being set holds ex_sup_of f .: x,L ) holds

rng (netmap ((FinSups f),L)) c= finsups (rng f)

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

assume A1: for x being set holds ex_sup_of f .: x,L ; :: thesis: rng (netmap ((FinSups f),L)) c= finsups (rng f)

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

set h = netmap ((FinSups f),L);

assume q in rng (netmap ((FinSups f),L)) ; :: thesis: q in finsups (rng f)

then consider x being object such that

A2: x in dom (netmap ((FinSups f),L)) and

A3: (netmap ((FinSups f),L)) . x = q by FUNCT_1:def 3;

A4: ex g being Function of (Fin J), the carrier of L st

for x being Element of Fin J holds

( g . x = sup (f .: x) & FinSups f = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) by Def2;

then reconsider x = x as Element of Fin J by A2;

A5: ( f .: x is finite Subset of (rng f) & ex_sup_of f .: x,L ) by A1, RELAT_1:111;

(netmap ((FinSups f),L)) . x = sup (f .: x) by A4;

hence q in finsups (rng f) by A3, A5; :: thesis: verum

for f being Function of J, the carrier of L st ( for x being set holds ex_sup_of f .: x,L ) holds

rng (netmap ((FinSups f),L)) c= finsups (rng f)

let J be set ; :: thesis: for f being Function of J, the carrier of L st ( for x being set holds ex_sup_of f .: x,L ) holds

rng (netmap ((FinSups f),L)) c= finsups (rng f)

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

assume A1: for x being set holds ex_sup_of f .: x,L ; :: thesis: rng (netmap ((FinSups f),L)) c= finsups (rng f)

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

set h = netmap ((FinSups f),L);

assume q in rng (netmap ((FinSups f),L)) ; :: thesis: q in finsups (rng f)

then consider x being object such that

A2: x in dom (netmap ((FinSups f),L)) and

A3: (netmap ((FinSups f),L)) . x = q by FUNCT_1:def 3;

A4: ex g being Function of (Fin J), the carrier of L st

for x being Element of Fin J holds

( g . x = sup (f .: x) & FinSups f = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) by Def2;

then reconsider x = x as Element of Fin J by A2;

A5: ( f .: x is finite Subset of (rng f) & ex_sup_of f .: x,L ) by A1, RELAT_1:111;

(netmap ((FinSups f),L)) . x = sup (f .: x) by A4;

hence q in finsups (rng f) by A3, A5; :: thesis: verum