let C1, C2 be non empty set ; :: thesis: for f, g being RMembership_Func of C1,C2 holds converse (max (f,g)) = max ((converse f),(converse g))
let f, g be RMembership_Func of C1,C2; :: thesis: converse (max (f,g)) = max ((converse f),(converse g))
A1: dom (max ((converse f),(converse g))) = [:C2,C1:] by FUNCT_2:def 1;
A2: for c being Element of [:C2,C1:] st c in [:C2,C1:] holds
(converse (max (f,g))) . c = (max ((converse f),(converse g))) . c

proof

let c be Element of [:C2,C1:]; :: thesis: ( c in [:C2,C1:] implies (converse (max (f,g))) . c = (max ((converse f),(converse g))) . c )
assume c in [:C2,C1:] ; :: thesis: (converse (max (f,g))) . c = (max ((converse f),(converse g))) . c
consider y, x being object such that
A3: y in C2 and
A4: x in C1 and
A5: c = [y,x] by ZFMISC_1:def 2;
reconsider y = y, x = x as set by TARSKI:1;
A6: [x,y] in [:C1,C2:] by A3, A4, ZFMISC_1:87;
(converse (max (f,g))) . (y,x) = (max (f,g)) . (x,y) by A5, Def1
.= max ((f . (x,y)),(g . (x,y))) by A6, FUZZY_1:def 4
.= max (((converse f) . (y,x)),(g . (x,y))) by A5, Def1
.= max (((converse f) . (y,x)),((converse g) . (y,x))) by A5, Def1
.= (max ((converse f),(converse g))) . (y,x) by A5, FUZZY_1:def 4 ;
hence (converse (max (f,g))) . c = (max ((converse f),(converse g))) . c by A5; :: thesis: verum

end;

dom (converse (max (f,g))) = [:C2,C1:] by FUNCT_2:def 1;
hence converse (max (f,g)) = max ((converse f),(converse g)) by A1, A2, PARTFUN1:5; :: thesis: verum