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
proof
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;
hence A = B by A7, A8, FUNCT_2:12; :: thesis: verum