let X be set ; :: thesis: for Y being non empty set
for f being Function of X,Y
for A being Subset of X st f is bijective holds
(f .: A) ` = f .: (A ` )
let Y be non empty set ; :: thesis: for f being Function of X,Y
for A being Subset of X st f is bijective holds
(f .: A) ` = f .: (A ` )
let f be Function of X,Y; :: thesis: for A being Subset of X st f is bijective holds
(f .: A) ` = f .: (A ` )
let A be Subset of X; :: thesis: ( f is bijective implies (f .: A) ` = f .: (A ` ) )
assume f is bijective ; :: thesis: (f .: A) ` = f .: (A ` )
then ( (f .: A) ` c= f .: (A ` ) & f .: (A ` ) c= (f .: A) ` ) by Th3, Th4;
hence (f .: A) ` = f .: (A ` ) by XBOOLE_0:def 10; :: thesis: verum