let X be set ; :: thesis: for f being Function of (bool X),(bool X) holds Flip (Flip f) = f
let f be Function of (bool X),(bool X); :: thesis: Flip (Flip f) = f
set g = Flip (Flip f);
for x being Subset of X holds (Flip (Flip f)) . x = f . x

proof

let x be Subset of X; :: thesis: (Flip (Flip f)) . x = f . x
(Flip (Flip f)) . x = ((Flip f) . (x `)) ` by Def14
.= ((f . ((x `) `)) `) ` by Def14
.= f . x ;
hence (Flip (Flip f)) . x = f . x ; :: thesis: verum

end;

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