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

for f being Function of J, the carrier of L st ex_sup_of rng f,L & ex_sup_of rng (netmap ((FinSups f),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) holds

Sup = sup (FinSups f)

let J be set ; :: thesis: for f being Function of J, the carrier of L st ex_sup_of rng f,L & ex_sup_of rng (netmap ((FinSups f),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) holds

Sup = sup (FinSups f)

let f be Function of J, the carrier of L; :: thesis: ( ex_sup_of rng f,L & ex_sup_of rng (netmap ((FinSups f),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) implies Sup = sup (FinSups f) )

assume that

A1: ex_sup_of rng f,L and

A2: ex_sup_of rng (netmap ((FinSups f),L)),L and

A3: for x being Element of Fin J holds ex_sup_of f .: x,L ; :: thesis: Sup = sup (FinSups f)

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

A4: "\/" ((rng f),L) <= sup (rng (netmap ((FinSups f),L))) by A1, A2, Th25, YELLOW_0:34;

rng (netmap ((FinSups f),L)) is_<=_than "\/" ((rng f),L)

thus Sup = "\/" ((rng f),L) by YELLOW_2:def 5

.= sup (rng (netmap ((FinSups f),L))) by A4, A8, ORDERS_2:2

.= sup (FinSups f) by YELLOW_2:def 5 ; :: thesis: verum

for f being Function of J, the carrier of L st ex_sup_of rng f,L & ex_sup_of rng (netmap ((FinSups f),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) holds

Sup = sup (FinSups f)

let J be set ; :: thesis: for f being Function of J, the carrier of L st ex_sup_of rng f,L & ex_sup_of rng (netmap ((FinSups f),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) holds

Sup = sup (FinSups f)

let f be Function of J, the carrier of L; :: thesis: ( ex_sup_of rng f,L & ex_sup_of rng (netmap ((FinSups f),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) implies Sup = sup (FinSups f) )

assume that

A1: ex_sup_of rng f,L and

A2: ex_sup_of rng (netmap ((FinSups f),L)),L and

A3: for x being Element of Fin J holds ex_sup_of f .: x,L ; :: thesis: Sup = sup (FinSups f)

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

A4: "\/" ((rng f),L) <= sup (rng (netmap ((FinSups f),L))) by A1, A2, Th25, YELLOW_0:34;

rng (netmap ((FinSups f),L)) is_<=_than "\/" ((rng f),L)

proof

then A8:
sup (rng (netmap ((FinSups f),L))) <= "\/" ((rng f),L)
by A2, YELLOW_0:def 9;
let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in rng (netmap ((FinSups f),L)) or a <= "\/" ((rng f),L) )

assume a in rng (netmap ((FinSups f),L)) ; :: thesis: a <= "\/" ((rng f),L)

then consider x being object such that

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

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

A7: 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 A5;

ex_sup_of f .: x,L by A3;

then sup (f .: x) <= "\/" ((rng f),L) by A1, RELAT_1:111, YELLOW_0:34;

hence a <= "\/" ((rng f),L) by A6, A7; :: thesis: verum

end;assume a in rng (netmap ((FinSups f),L)) ; :: thesis: a <= "\/" ((rng f),L)

then consider x being object such that

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

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

A7: 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 A5;

ex_sup_of f .: x,L by A3;

then sup (f .: x) <= "\/" ((rng f),L) by A1, RELAT_1:111, YELLOW_0:34;

hence a <= "\/" ((rng f),L) by A6, A7; :: thesis: verum

thus Sup = "\/" ((rng f),L) by YELLOW_2:def 5

.= sup (rng (netmap ((FinSups f),L))) by A4, A8, ORDERS_2:2

.= sup (FinSups f) by YELLOW_2:def 5 ; :: thesis: verum