let X be non empty set ; :: thesis: for R being RMembership_Func of X,X holds (Imf X,X) (#) R = R
let R be RMembership_Func of X,X; :: thesis: (Imf X,X) (#) R = R
A1: dom ((Imf X,X) (#) R) = [:X,X:] by FUNCT_2:def 1
.= dom R by FUNCT_2:def 1 ;
for x, y being set st [x,y] in dom ((Imf X,X) (#) R) holds
((Imf X,X) (#) R) . x,y = R . x,y

proof

let x, y be set ; :: thesis: ( [x,y] in dom ((Imf X,X) (#) R) implies ((Imf X,X) (#) R) . x,y = R . x,y )
assume [x,y] in dom ((Imf X,X) (#) R) ; :: thesis: ((Imf X,X) (#) R) . x,y = R . x,y
then reconsider x = x, y = y as Element of X by ZFMISC_1:106;
A2: ((Imf X,X) (#) R) . x,y = "\/" { (((Imf X,X) . x,z) "/\" (R . z,y)) where z is Element of X : verum } ,(RealPoset [.0 ,1.]) by LFUZZY_0:22;
set S = { (((Imf X,X) . x,z) "/\" (R . z,y)) where z is Element of X : verum } ;
A3: R . x,y is_>=_than { (((Imf X,X) . x,z) "/\" (R . z,y)) where z is Element of X : verum }

proof

for c being Element of (RealPoset [.0 ,1.]) st c in { (((Imf X,X) . x,z) "/\" (R . z,y)) where z is Element of X : verum } holds
c <<= R . [x,y]

proof

let c be Element of (RealPoset [.0 ,1.]); :: thesis: ( c in { (((Imf X,X) . x,z) "/\" (R . z,y)) where z is Element of X : verum } implies c <<= R . [x,y] )
assume c in { (((Imf X,X) . x,z) "/\" (R . z,y)) where z is Element of X : verum } ; :: thesis: c <<= R . [x,y]
then consider z being Element of X such that
A4: c = ((Imf X,X) . x,z) "/\" (R . z,y) ;

per cases ( x = z or x <> z ) ;

suppose A5: x = z ; :: thesis: c <<= R . [x,y]

A6: R . z,y <= 1 by FUZZY_4:4;
c = min (R . [z,y]),1 by A4, A5, FUZZY_4:25
.= R . [x,y] by A5, A6, XXREAL_0:def 9 ;
hence c <<= R . [x,y] by LFUZZY_0:3; :: thesis: verum

end;

suppose A7: x <> z ; :: thesis: c <<= R . [x,y]

A8: 0 <= R . z,y by FUZZY_4:4;
c = min (R . [z,y]),0 by A4, A7, FUZZY_4:25
.= 0 by A8, XXREAL_0:def 9 ;
then c <= R . x,y by FUZZY_4:4;
hence c <<= R . [x,y] by LFUZZY_0:3; :: thesis: verum

end;

end;

end;

hence R . x,y is_>=_than { (((Imf X,X) . x,z) "/\" (R . z,y)) where z is Element of X : verum } by LATTICE3:def 9; :: thesis: verum

end;

for b being Element of (RealPoset [.0 ,1.]) st b is_>=_than { (((Imf X,X) . x,z) "/\" (R . z,y)) where z is Element of X : verum } holds
R . x,y <<= b

proof

let b be Element of (RealPoset [.0 ,1.]); :: thesis: ( b is_>=_than { (((Imf X,X) . x,z) "/\" (R . z,y)) where z is Element of X : verum } implies R . x,y <<= b )
assume A9: b is_>=_than { (((Imf X,X) . x,z) "/\" (R . z,y)) where z is Element of X : verum } ; :: thesis: R . x,y <<= b
A10: R . x,y <= 1 by FUZZY_4:4;
((Imf X,X) . x,x) "/\" (R . [x,y]) = min 1,(R . x,y) by FUZZY_4:25
.= R . [x,y] by A10, XXREAL_0:def 9 ;
then R . x,y in { (((Imf X,X) . x,z) "/\" (R . z,y)) where z is Element of X : verum } ;
hence R . x,y <<= b by A9, LATTICE3:def 9; :: thesis: verum

end;

hence ((Imf X,X) (#) R) . x,y = R . x,y by A2, A3, YELLOW_0:32; :: thesis: verum

end;

hence (Imf X,X) (#) R = R by A1, BINOP_1:32; :: thesis: verum