let C be non empty set ; :: thesis: for f, g being Membership_Func of C st g c= & f c= holds
f = g
let f, g be Membership_Func of C; :: thesis: ( g c= & f c= implies f = g )
set A = f;
set B = g;
assume A1: ( g c= & f c= ) ; :: thesis: f = g
A2: for c being Element of C st c in C holds
f . c = g . c

proof

let c be Element of C; :: thesis: ( c in C implies f . c = g . c )
( f . c <= g . c & g . c <= f . c ) by A1;
hence ( c in C implies f . c = g . c ) by XXREAL_0:1; :: thesis: verum

end;

( C = dom f & C = dom g ) by FUNCT_2:def 1;
hence f = g by A2, PARTFUN1:5; :: thesis: verum