let R be non empty RelStr ; :: thesis: for f, g being map of R holds Flip (f * g) = (Flip f) * (Flip g)
let f, g be map of R; :: thesis: Flip (f * g) = (Flip f) * (Flip g)
set fg = Flip (f * g);
set ff = Flip f;
set gg = Flip g;
for x being Subset of R holds (Flip (f * g)) . x = ((Flip f) * (Flip g)) . x

proof

let x be Subset of R; :: thesis: (Flip (f * g)) . x = ((Flip f) * (Flip g)) . x
x ` in bool the carrier of R ;
then A1: x ` in dom g by FUNCT_2:def 1;
a2: dom (Flip g) = bool the carrier of R by FUNCT_2:def 1;
(Flip (f * g)) . x = ((f * g) . (x `)) ` by ROUGHS_2:def 14
.= (f . (((g . (x `)) `) `)) ` by FUNCT_1:13, A1
.= (Flip f) . ((g . (x `)) `) by ROUGHS_2:def 14
.= (Flip f) . ((Flip g) . x) by ROUGHS_2:def 14
.= ((Flip f) * (Flip g)) . x by a2, FUNCT_1:13 ;
hence (Flip (f * g)) . x = ((Flip f) * (Flip g)) . x ; :: thesis: verum

end;

hence Flip (f * g) = (Flip f) * (Flip g) ; :: thesis: verum