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 set 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:106;
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:34; :: thesis: verum