let C1, C2 be non empty set ; :: thesis: for f, g being RMembership_Func of C1,C2 holds converse (min f,g) = min (converse f),(converse g)
let f, g be RMembership_Func of C1,C2; :: thesis: converse (min f,g) = min (converse f),(converse g)
A1: dom (min (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 (min f,g)) . c = (min (converse f),(converse g)) . c

proof

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

end;

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