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