let IT be RMembership_Func of C1,C2; :: thesis: ( IT = converse iff for x, y being set st [x,y] in [:C1,C2:] holds
IT . x,y = h . y,x )
A4: dom h = [:C2,C1:] by FUNCT_2:def 1;
thus ( IT = ~ h implies for x, y being set st [x,y] in [:C1,C2:] holds
IT . x,y = h . y,x ) :: thesis: ( ( for x, y being set st [x,y] in [:C1,C2:] holds
IT . x,y = h . y,x ) implies IT = converse )

proof

assume A5: IT = ~ h ; :: thesis: for x, y being set st [x,y] in [:C1,C2:] holds
IT . x,y = h . y,x
let x, y be set ; :: thesis: ( [x,y] in [:C1,C2:] implies IT . x,y = h . y,x )
assume [x,y] in [:C1,C2:] ; :: thesis: IT . x,y = h . y,x
then [y,x] in dom h by A4, ZFMISC_1:107;
hence IT . x,y = h . y,x by A5, FUNCT_4:def 2; :: thesis: verum

end;

A6: dom IT = [:C1,C2:] by FUNCT_2:def 1;
A7: for x being set holds
( x in dom IT iff ex y, z being set st
( x = [z,y] & [y,z] in dom h ) )

proof

let x be set ; :: thesis: ( x in dom IT iff ex y, z being set st
( x = [z,y] & [y,z] in dom h ) )
thus ( x in dom IT implies ex y, z being set st
( x = [z,y] & [y,z] in dom h ) ) :: thesis: ( ex y, z being set st
( x = [z,y] & [y,z] in dom h ) implies x in dom IT )

proof

assume x in dom IT ; :: thesis: ex y, z being set st
( x = [z,y] & [y,z] in dom h )
then consider z, y being set such that
A8: z in C1 and
A9: y in C2 and
A10: x = [z,y] by ZFMISC_1:def 2;
take y ; :: thesis: ex z being set st
( x = [z,y] & [y,z] in dom h )
take z ; :: thesis: ( x = [z,y] & [y,z] in dom h )
thus ( x = [z,y] & [y,z] in dom h ) by A4, A8, A9, A10, ZFMISC_1:def 2; :: thesis: verum

end;

thus ( ex y, z being set st
( x = [z,y] & [y,z] in dom h ) implies x in dom IT ) by A6, ZFMISC_1:107; :: thesis: verum

end;

assume for x, y being set st [x,y] in [:C1,C2:] holds
IT . x,y = h . y,x ; :: thesis: IT = converse
then for y, z being set st [y,z] in dom h holds
IT . z,y = h . y,z by ZFMISC_1:107;
hence IT = converse by A7, FUNCT_4:def 2; :: thesis: verum