let A, B be prenet of L; :: thesis: ( 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) & A = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) & 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) & B = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) implies A = B )

assume that

A5: 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) & A = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) and

A6: 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) & B = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) ; :: thesis: A = B

consider g1 being Function of (Fin J), the carrier of L such that

A7: for x being Element of Fin J holds

( g1 . x = sup (f .: x) & A = NetStr(# (Fin J),(RelIncl (Fin J)),g1 #) ) by A5;

consider g2 being Function of (Fin J), the carrier of L such that

A8: for x being Element of Fin J holds

( g2 . x = sup (f .: x) & B = NetStr(# (Fin J),(RelIncl (Fin J)),g2 #) ) by A6;

for x being object st x in Fin J holds

g1 . x = g2 . x

for x being Element of Fin J holds

( g . x = sup (f .: x) & A = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) & 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) & B = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) implies A = B )

assume that

A5: 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) & A = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) and

A6: 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) & B = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) ; :: thesis: A = B

consider g1 being Function of (Fin J), the carrier of L such that

A7: for x being Element of Fin J holds

( g1 . x = sup (f .: x) & A = NetStr(# (Fin J),(RelIncl (Fin J)),g1 #) ) by A5;

consider g2 being Function of (Fin J), the carrier of L such that

A8: for x being Element of Fin J holds

( g2 . x = sup (f .: x) & B = NetStr(# (Fin J),(RelIncl (Fin J)),g2 #) ) by A6;

for x being object st x in Fin J holds

g1 . x = g2 . x

proof

hence
A = B
by A7, A8, FUNCT_2:12; :: thesis: verum
let x be object ; :: thesis: ( x in Fin J implies g1 . x = g2 . x )

assume A9: x in Fin J ; :: thesis: g1 . x = g2 . x

reconsider xx = x as set by TARSKI:1;

thus g1 . x = sup (f .: xx) by A7, A9

.= g2 . x by A8, A9 ; :: thesis: verum

end;assume A9: x in Fin J ; :: thesis: g1 . x = g2 . x

reconsider xx = x as set by TARSKI:1;

thus g1 . x = sup (f .: xx) by A7, A9

.= g2 . x by A8, A9 ; :: thesis: verum