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 :: thesis: for x being object holds
( ( x in (Inv f) " A implies x in f " (Inv A) ) & ( x in f " (Inv A) implies x in (Inv f) " A ) )

let x be object ; :: thesis: ( ( x in (Inv f) " A implies x in f " (Inv A) ) & ( x in f " (Inv A) implies x in (Inv f) " A ) )
reconsider xx = x as set by TARSKI:1;

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

A1: (Inv f) . x = (f . xx) " by VALUED_1:10;
assume A2: x in (Inv f) " A ; :: thesis: x in f " (Inv A)
then (Inv f) . x in A by FUNCT_2:38;
then 1 / ((f . xx) ") in Inv A by A1;
hence x in f " (Inv A) by A2, FUNCT_2:38; :: thesis: verum

end;

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

end;

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