let X, Y be set ; :: thesis: for f being Function st f " X = f " Y & X c= rng f & Y c= rng f holds
X = Y
let f be Function; :: thesis: ( f " X = f " Y & X c= rng f & Y c= rng f implies X = Y )
assume ( f " X = f " Y & X c= rng f & Y c= rng f ) ; :: thesis: X = Y
then ( X c= Y & Y c= X ) by Th158;
hence X = Y by XBOOLE_0:def 10; :: thesis: verum