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)
set h = netmap (FinSups f),L;
consider g being Function of (Fin J),the carrier of L such that
A2: for x being Element of Fin J holds
( g . x = sup (f .: x) & FinSups f = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) by Def2;
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in rng (netmap (FinSups f),L) or q in finsups (rng f) )
assume q in rng (netmap (FinSups f),L) ; :: thesis: q in finsups (rng f)
then consider x being set such that
A3: ( x in dom (netmap (FinSups f),L) & (netmap (FinSups f),L) . x = q ) by FUNCT_1:def 5;
reconsider x = x as Element of Fin J by A2, A3;
A4: (netmap (FinSups f),L) . x = sup (f .: x) by A2;
A5: f .: x is finite Subset of (rng f) by RELAT_1:144;
ex_sup_of f .: x,L by A1;
hence q in finsups (rng f) by A3, A4, A5; :: thesis: verum