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: 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 set such that
A2: ( x in C1 & y in C2 & c = [x,y] ) by ZFMISC_1:def 2;
A3: [y,x] in [:C2,C1:] by A2, ZFMISC_1:106;
(converse (converse f)) . x,y = (converse f) . y,x by A2, Def1
.= f . x,y by A3, Def1 ;
hence (converse (converse f)) . c = f . c by A2; :: thesis: verum

end;

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