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

proof

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

end;

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