let X be set ; for Y being non empty set
for f being Function of X,Y
for A being Subset of X st f is one-to-one holds
f .: (A `) c= (f .: A) `
let Y be non empty set ; for f being Function of X,Y
for A being Subset of X st f is one-to-one holds
f .: (A `) c= (f .: A) `
let f be Function of X,Y; for A being Subset of X st f is one-to-one holds
f .: (A `) c= (f .: A) `
let A be Subset of X; ( f is one-to-one implies f .: (A `) c= (f .: A) ` )
assume A1:
f is one-to-one
; f .: (A `) c= (f .: A) `
let e be object ; TARSKI:def 3 ( not e in f .: (A `) or e in (f .: A) ` )
assume A2:
e in f .: (A `)
; e in (f .: A) `
then reconsider y = e as Element of Y ;
consider x1 being object such that
A3:
x1 in X
and
A4:
x1 in A `
and
A5:
y = f . x1
by A2, FUNCT_2:64;
assume
not e in (f .: A) `
; contradiction
then A6:
ex x2 being object st
( x2 in X & x2 in A & y = f . x2 )
by FUNCT_2:64, SUBSET_1:29;
not x1 in A
by A4, XBOOLE_0:def 5;
hence
contradiction
by A1, A3, A5, A6, FUNCT_2:19; verum