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 )
proof
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
proof
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;
hence p .: x1 <> p .: x2 by A2, A4, FUNCT_1:def 6; :: thesis: verum
end;
A6: ( not x2 c= x1 implies p .: x1 <> p .: x2 )
proof
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
proof
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;
hence p .: x1 <> p .: x2 by A2, A7, FUNCT_1:def 6; :: thesis: verum
end;
assume x1 <> x2 ; :: thesis: p .: x1 <> p .: x2
hence p .: x1 <> p .: x2 by A3, A6, XBOOLE_0:def 10; :: thesis: verum