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

proof

let c be Element of [:C3,C1:]; :: thesis: ( c in [:C3,C1:] implies (converse (f (#) g)) . c = ((converse g) (#) (converse f)) . c )
assume c in [:C3,C1:] ; :: thesis: (converse (f (#) g)) . c = ((converse g) (#) (converse f)) . c
consider z, x being object such that
A3: z in C3 and
A4: x in C1 and
A5: c = [z,x] by ZFMISC_1:def 2;
A6: [x,z] in [:C1,C3:] by A3, A4, ZFMISC_1:87;
reconsider z = z, x = x as set by TARSKI:1;
A7: ((converse g) (#) (converse f)) . (z,x) = upper_bound (rng (min ((converse g),(converse f),z,x))) by A5, Def3;
(converse (f (#) g)) . (z,x) = (f (#) g) . (x,z) by A5, Def1
.= upper_bound (rng (min (f,g,x,z))) by A6, Def3 ;
hence (converse (f (#) g)) . c = ((converse g) (#) (converse f)) . c by A3, A4, A5, A7, Lm5; :: thesis: verum

end;

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