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 set ; :: 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 set such that
A2: x in dom (netmap (FinSups f),L) and
A3: (netmap (FinSups f),L) . x = q by FUNCT_1:def 5;
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:144;
(netmap (FinSups f),L) . x = sup (f .: x) by A4;
hence q in finsups (rng f) by A3, A5; :: thesis: verum