let X be set ; :: thesis: for f being Function of (bool X),(bool X) st f . X = X holds

(Flip f) . {} = {}

let f be Function of (bool X),(bool X); :: thesis: ( f . X = X implies (Flip f) . {} = {} )

assume A1: f . X = X ; :: thesis: (Flip f) . {} = {}

set y = {} X;

(Flip f) . ({} X) = (f . (({} X) `)) ` by Def14

.= {} X by A1 ;

hence (Flip f) . {} = {} ; :: thesis: verum

(Flip f) . {} = {}

let f be Function of (bool X),(bool X); :: thesis: ( f . X = X implies (Flip f) . {} = {} )

assume A1: f . X = X ; :: thesis: (Flip f) . {} = {}

set y = {} X;

(Flip f) . ({} X) = (f . (({} X) `)) ` by Def14

.= {} X by A1 ;

hence (Flip f) . {} = {} ; :: thesis: verum