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
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) & A = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) and
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) & B = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) ; :: thesis: A = B
consider g1 being Function of (Fin J),the carrier of L such that
A6: for x being Element of Fin J holds
( g1 . x = sup (f .: x) & A = NetStr(# (Fin J),(RelIncl (Fin J)),g1 #) ) by A4;
consider g2 being Function of (Fin J),the carrier of L such that
A7: for x being Element of Fin J holds
( g2 . x = sup (f .: x) & B = NetStr(# (Fin J),(RelIncl (Fin J)),g2 #) ) by A5;
for x being set st x in Fin J holds
g1 . x = g2 . x

proof

let x be set ; :: thesis: ( x in Fin J implies g1 . x = g2 . x )
assume A8: x in Fin J ; :: thesis: g1 . x = g2 . x
hence g1 . x = sup (f .: x) by A6
.= g2 . x by A7, A8 ;
:: thesis: verum

end;

hence A = B by A6, A7, FUNCT_2:18; :: thesis: verum