let C be non empty set ; :: thesis: for f, h, g being Membership_Func of C st g c= & h c= & min (g,h) = EMF C holds

f = EMF C

let f, h, g be Membership_Func of C; :: thesis: ( g c= & h c= & min (g,h) = EMF C implies f = EMF C )

assume that

A1: ( g c= & h c= ) and

A2: min (g,h) = EMF C ; :: thesis: f = EMF C

A3: for x being Element of C st x in C holds

f . x = (EMF C) . x

hence f = EMF C by A3, PARTFUN1:5; :: thesis: verum

f = EMF C

let f, h, g be Membership_Func of C; :: thesis: ( g c= & h c= & min (g,h) = EMF C implies f = EMF C )

assume that

A1: ( g c= & h c= ) and

A2: min (g,h) = EMF C ; :: thesis: f = EMF C

A3: for x being Element of C st x in C holds

f . x = (EMF C) . x

proof

( C = dom f & C = dom (EMF C) )
by FUNCT_2:def 1;
let x be Element of C; :: thesis: ( x in C implies f . x = (EMF C) . x )

( f . x <= g . x & f . x <= h . x ) by A1;

then f . x <= min ((g . x),(h . x)) by XXREAL_0:20;

then A4: f . x <= (min (g,h)) . x by Def3;

(EMF C) . x <= f . x by Th15;

hence ( x in C implies f . x = (EMF C) . x ) by A2, A4, XXREAL_0:1; :: thesis: verum

end;( f . x <= g . x & f . x <= h . x ) by A1;

then f . x <= min ((g . x),(h . x)) by XXREAL_0:20;

then A4: f . x <= (min (g,h)) . x by Def3;

(EMF C) . x <= f . x by Th15;

hence ( x in C implies f . x = (EMF C) . x ) by A2, A4, XXREAL_0:1; :: thesis: verum

hence f = EMF C by A3, PARTFUN1:5; :: thesis: verum