let A be non empty set ; :: thesis: for f, g being Function of (bool A),(bool A) st f cc= g holds
Flip g cc= Flip f
let f, g be Function of (bool A),(bool A); :: thesis: ( f cc= g implies Flip g cc= Flip f )
assume A1: f cc= g ; :: thesis: Flip g cc= Flip f
set ff = Flip f;
set gg = Flip g;
a2: dom (Flip f) = bool A by FUNCT_2:def 1;
for x being set st x in dom (Flip g) holds
(Flip g) . x c= (Flip f) . x

proof

let x be set ; :: thesis: ( x in dom (Flip g) implies (Flip g) . x c= (Flip f) . x )
assume x in dom (Flip g) ; :: thesis: (Flip g) . x c= (Flip f) . x
then reconsider xx = x as Subset of A ;
B1: (Flip g) . xx = (g . (xx `)) ` by ROUGHS_2:def 14;
B2: (Flip f) . xx = (f . (xx `)) ` by ROUGHS_2:def 14;
dom f = bool A by FUNCT_2:def 1;
then f . (xx `) c= g . (xx `) by A1, ALTCAT_2:def 1;
hence (Flip g) . x c= (Flip f) . x by B1, B2, SUBSET_1:12; :: thesis: verum

end;

hence Flip g cc= Flip f by a2, ALTCAT_2:def 1; :: thesis: verum