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

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

hence
Flip (f * g) = (Flip f) * (Flip g)
; :: thesis: verum
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;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