let X be set ; :: thesis: for A being without_zero Subset of REAL
for f being Function of X,REAL holds (Inv f) " A = f " (Inv A)
let A be without_zero Subset of REAL ; :: thesis: for f being Function of X,REAL holds (Inv f) " A = f " (Inv A)
let f be Function of X,REAL ; :: thesis: (Inv f) " A = f " (Inv A)

now

let x be set ; :: thesis: ( ( x in (Inv f) " A implies x in f " (Inv A) ) & ( x in f " (Inv A) implies x in (Inv f) " A ) )
A1: (f . x) " = 1 / (f . x) ;

hereby :: thesis: ( x in f " (Inv A) implies x in (Inv f) " A )

assume A2: x in (Inv f) " A ; :: thesis: x in f " (Inv A)
then A3: ( x in X & (Inv f) . x in A ) by FUNCT_2:46;
(Inv f) . x = (f . x) " by VALUED_1:10;
then 1 / ((f . x) " ) in Inv A by A3;
then f . x in Inv A ;
hence x in f " (Inv A) by A2, FUNCT_2:46; :: thesis: verum

end;

assume A4: x in f " (Inv A) ; :: thesis: x in (Inv f) " A
then A5: ( x in X & f . x in Inv A ) by FUNCT_2:46;
(Inv f) . x = (f . x) " by VALUED_1:10;
then (Inv f) . x in Inv (Inv A) by A1, A5;
hence x in (Inv f) " A by A4, FUNCT_2:46; :: thesis: verum

end;

hence (Inv f) " A = f " (Inv A) by TARSKI:2; :: thesis: verum