let X be set ; :: thesis: for Y being non empty set

for p being Function of X,Y st p is one-to-one holds

for x1, x2 being Subset of X st x1 <> x2 holds

p .: x1 <> p .: x2

let Y be non empty set ; :: thesis: for p being Function of X,Y st p is one-to-one holds

for x1, x2 being Subset of X st x1 <> x2 holds

p .: x1 <> p .: x2

let p be Function of X,Y; :: thesis: ( p is one-to-one implies for x1, x2 being Subset of X st x1 <> x2 holds

p .: x1 <> p .: x2 )

assume A1: p is one-to-one ; :: thesis: for x1, x2 being Subset of X st x1 <> x2 holds

p .: x1 <> p .: x2

let x1, x2 be Subset of X; :: thesis: ( x1 <> x2 implies p .: x1 <> p .: x2 )

A2: X = dom p by FUNCT_2:def 1;

A3: ( not x1 c= x2 implies p .: x1 <> p .: x2 )

hence p .: x1 <> p .: x2 by A3, A6, XBOOLE_0:def 10; :: thesis: verum

for p being Function of X,Y st p is one-to-one holds

for x1, x2 being Subset of X st x1 <> x2 holds

p .: x1 <> p .: x2

let Y be non empty set ; :: thesis: for p being Function of X,Y st p is one-to-one holds

for x1, x2 being Subset of X st x1 <> x2 holds

p .: x1 <> p .: x2

let p be Function of X,Y; :: thesis: ( p is one-to-one implies for x1, x2 being Subset of X st x1 <> x2 holds

p .: x1 <> p .: x2 )

assume A1: p is one-to-one ; :: thesis: for x1, x2 being Subset of X st x1 <> x2 holds

p .: x1 <> p .: x2

let x1, x2 be Subset of X; :: thesis: ( x1 <> x2 implies p .: x1 <> p .: x2 )

A2: X = dom p by FUNCT_2:def 1;

A3: ( not x1 c= x2 implies p .: x1 <> p .: x2 )

proof

A6:
( not x2 c= x1 implies p .: x1 <> p .: x2 )
assume
not x1 c= x2
; :: thesis: p .: x1 <> p .: x2

then consider a being object such that

A4: a in x1 and

A5: not a in x2 ;

not p . a in p .: x2

end;then consider a being object such that

A4: a in x1 and

A5: not a in x2 ;

not p . a in p .: x2

proof

hence
p .: x1 <> p .: x2
by A2, A4, FUNCT_1:def 6; :: thesis: verum
assume
p . a in p .: x2
; :: thesis: contradiction

then ex b being object st

( b in dom p & b in x2 & p . a = p . b ) by FUNCT_1:def 6;

hence contradiction by A1, A2, A4, A5; :: thesis: verum

end;then ex b being object st

( b in dom p & b in x2 & p . a = p . b ) by FUNCT_1:def 6;

hence contradiction by A1, A2, A4, A5; :: thesis: verum

proof

assume
x1 <> x2
; :: thesis: p .: x1 <> p .: x2
assume
not x2 c= x1
; :: thesis: p .: x1 <> p .: x2

then consider a being object such that

A7: a in x2 and

A8: not a in x1 ;

not p . a in p .: x1

end;then consider a being object such that

A7: a in x2 and

A8: not a in x1 ;

not p . a in p .: x1

proof

hence
p .: x1 <> p .: x2
by A2, A7, FUNCT_1:def 6; :: thesis: verum
assume
p . a in p .: x1
; :: thesis: contradiction

then ex b being object st

( b in dom p & b in x1 & p . a = p . b ) by FUNCT_1:def 6;

hence contradiction by A1, A2, A7, A8; :: thesis: verum

end;then ex b being object st

( b in dom p & b in x1 & p . a = p . b ) by FUNCT_1:def 6;

hence contradiction by A1, A2, A7, A8; :: thesis: verum

hence p .: x1 <> p .: x2 by A3, A6, XBOOLE_0:def 10; :: thesis: verum