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

for f being Function of J, the carrier of L holds

( x is Element of (FinSups f) iff x is Element of Fin J )

let J, x be set ; :: thesis: for f being Function of J, the carrier of L holds

( x is Element of (FinSups f) iff x is Element of Fin J )

let f be Function of J, the carrier of L; :: thesis: ( x is Element of (FinSups f) iff x is Element of Fin J )

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;

hence ( x is Element of (FinSups f) iff x is Element of Fin J ) ; :: thesis: verum

for f being Function of J, the carrier of L holds

( x is Element of (FinSups f) iff x is Element of Fin J )

let J, x be set ; :: thesis: for f being Function of J, the carrier of L holds

( x is Element of (FinSups f) iff x is Element of Fin J )

let f be Function of J, the carrier of L; :: thesis: ( x is Element of (FinSups f) iff x is Element of Fin J )

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;

hence ( x is Element of (FinSups f) iff x is Element of Fin J ) ; :: thesis: verum