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

proof

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

proof

for c being Element of (RealPoset [.0 ,1.]) st c in { ((R . x,z) "/\" ((Imf X,X) . 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 { ((R . x,z) "/\" ((Imf X,X) . z,y)) where z is Element of X : verum } implies c <<= R . [x,y] )
assume c in { ((R . x,z) "/\" ((Imf X,X) . 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 = (R . x,z) "/\" ((Imf X,X) . z,y) ;

per cases ( y = z or not y = z ) ;

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

A6: R . x,z <= 1 by FUZZY_4:4;
c = min (R . [x,z]),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: not y = z ; :: thesis: c <<= R . [x,y]

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

end;

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

end;

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