let X be set ; :: thesis: for f being Function of (bool X),(bool X) st ( for A, B being Subset of X holds f . (A /\ B) = (f . A) /\ (f . B) ) holds
for A, B being Subset of X holds (Flip f) . (A \/ B) = ((Flip f) . A) \/ ((Flip f) . B)
let f be Function of (bool X),(bool X); :: thesis: ( ( for A, B being Subset of X holds f . (A /\ B) = (f . A) /\ (f . B) ) implies for A, B being Subset of X holds (Flip f) . (A \/ B) = ((Flip f) . A) \/ ((Flip f) . B) )
assume A1: for A, B being Subset of X holds f . (A /\ B) = (f . A) /\ (f . B) ; :: thesis: for A, B being Subset of X holds (Flip f) . (A \/ B) = ((Flip f) . A) \/ ((Flip f) . B)
let A, B be Subset of X; :: thesis: (Flip f) . (A \/ B) = ((Flip f) . A) \/ ((Flip f) . B)
set g = Flip f;
(Flip f) . (A \/ B) = (f . ((A \/ B) `)) ` by Def14
.= (f . ((A `) /\ (B `))) ` by XBOOLE_1:53
.= ((f . (A `)) /\ (f . (B `))) ` by A1
.= ((f . (A `)) `) \/ ((f . (B `)) `) by XBOOLE_1:54
.= ((Flip f) . A) \/ ((f . (B `)) `) by Def14
.= ((Flip f) . A) \/ ((Flip f) . B) by Def14 ;
hence (Flip f) . (A \/ B) = ((Flip f) . A) \/ ((Flip f) . B) ; :: thesis: verum