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 (f (#) g)) = [:C3,C1:] & dom ((converse g) (#) (converse f)) = [:C3,C1:] )
by FUNCT_2:def 1;
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 A2:
(
z in C3 &
x in C1 &
c = [z,x] )
by ZFMISC_1:def 2;
A3:
[x,z] in [:C1,C3:]
by A2, ZFMISC_1:106;
A4:
(converse (f (#) g)) . z,
x =
(f (#) g) . x,
z
by A2, Def1
.=
sup (rng (min f,g,x,z))
by A3, Def3
;
((converse g) (#) (converse f)) . z,
x = sup (rng (min (converse g),(converse f),z,x))
by A2, Def3;
hence
(converse (f (#) g)) . c = ((converse g) (#) (converse f)) . c
by A2, A4, Lm5;
:: thesis: verum
end;
hence
converse (f (#) g) = (converse g) (#) (converse f)
by A1, PARTFUN1:34; :: thesis: verum