set IT = converse ;
A1: dom h = [:C2,C1:] by FUNCT_2:def 1;
then A2: dom (converse ) = [:C1,C2:] by FUNCT_4:46;
rng h c= [.0,1.] by RELAT_1:def 19;
then A3: rng (converse ) c= [.0,1.] by A1, FUNCT_4:47;
then rng (converse ) c= REAL by MEMBERED:3;
then reconsider IT = converse as PartFunc of [:C1,C2:],REAL by A2, RELSET_1:4;
IT is Membership_Func of [:C1,C2:] by A2, A3, FUNCT_2:def 1, RELAT_1:def 19;
hence converse is RMembership_Func of C1,C2 ; :: thesis: verum