let X1, X2 be set ; :: thesis: for f being Function st f .: X1 c= f .: X2 & X1 c= dom f & f is one-to-one holds
X1 c= X2
let f be Function; :: thesis: ( f .: X1 c= f .: X2 & X1 c= dom f & f is one-to-one implies X1 c= X2 )
assume that
A1: f .: X1 c= f .: X2 and
A2: X1 c= dom f and
A3: f is one-to-one ; :: thesis: X1 c= X2
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X1 or x in X2 )
assume A4: x in X1 ; :: thesis: x in X2
then f . x in f .: X1 by A2, Def6;
then ex x2 being object st
( x2 in dom f & x2 in X2 & f . x = f . x2 ) by A1, Def6;
hence x in X2 by A2, A3, A4; :: thesis: verum