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: for x, y being object st [x,y] in dom ((Imf (X,X)) (#) R) holds
((Imf (X,X)) (#) R) . (x,y) = R . (x,y)

proof

let x, y be object ; :: 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:87;
set S = { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } ;
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
A2: c = ((Imf (X,X)) . (x,z)) "/\" (R . (z,y)) ;

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

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

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

end;

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

A6: 0 <= R . (z,y) by FUZZY_4:4;
c = min ((R . [z,y]),0) by A2, A5, FUZZY_4:25
.= 0 by A6, 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;

then A7: ( ((Imf (X,X)) (#) R) . (x,y) = "\/" ( { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } ,(RealPoset [.0,1.])) & R . (x,y) is_>=_than { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } ) by LATTICE3:def 9, LFUZZY_0:22;
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 )
A8: 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 A8, XXREAL_0:def 9 ;
then A9: R . (x,y) in { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } ;
assume b is_>=_than { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } ; :: thesis: R . (x,y) <<= b
hence R . (x,y) <<= b by A9, LATTICE3:def 9; :: thesis: verum

end;

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

end;

dom ((Imf (X,X)) (#) R) = [:X,X:] by FUNCT_2:def 1
.= dom R by FUNCT_2:def 1 ;
hence (Imf (X,X)) (#) R = R by A1, BINOP_1:20; :: thesis: verum