let X, Y be non empty set ; :: thesis: for f being Function of X,Y st f is bijective holds
( .: f is bijective & ( for s being Subset of X holds (.: f) . s = f .: s ) )
let f be Function of X,Y; :: thesis: ( f is bijective implies ( .: f is bijective & ( for s being Subset of X holds (.: f) . s = f .: s ) ) )
assume A1: f is bijective ; :: thesis: ( .: f is bijective & ( for s being Subset of X holds (.: f) . s = f .: s ) )
A2: dom f = X by FUNCT_2:def 1;
for y being object st y in bool Y holds
ex x being object st
( x in bool X & y = (.: f) . x )

proof

let y be object ; :: thesis: ( y in bool Y implies ex x being object st
( x in bool X & y = (.: f) . x ) )
assume y in bool Y ; :: thesis: ex x being object st
( x in bool X & y = (.: f) . x )
then reconsider Z = y as Subset of (rng f) by A1, FUNCT_2:def 3;
A3: f .: (f " Z) = Z by FUNCT_1:77;
take x = f " Z; :: thesis: ( x in bool X & y = (.: f) . x )
thus ( x in bool X & y = (.: f) . x ) by A2, A3, FUNCT_3:def 1; :: thesis: verum

end;

then rng (.: f) = bool Y by FUNCT_2:10;
then .: f is onto by FUNCT_2:def 3;
hence .: f is bijective by A1; :: thesis: for s being Subset of X holds (.: f) . s = f .: s
thus for s being Subset of X holds (.: f) . s = f .: s by A2, FUNCT_3:def 1; :: thesis: verum