let X be set ; :: thesis: for f being Function of (bool X),(bool X) st f = id (bool X) holds
Flip f = f
let f be Function of (bool X),(bool X); :: thesis: ( f = id (bool X) implies Flip f = f )
assume A1: f = id (bool X) ; :: thesis: Flip f = f
for x being Subset of X holds (Flip f) . x = f . x

proof

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

end;

hence Flip f = f ; :: thesis: verum