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

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

hence
Flip g cc= Flip f
by a2, ALTCAT_2:def 1; :: thesis: verum
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;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