environ

 vocabularies ENUMSET, RELATION, RELAT_AB, FUNCT;
 notations ENUMSET, RELATION, RELAT_AB;
 constructors ENUMSET, RELATION, RELAT_AB;
 definitions ENUMSET, RELATION, RELAT_AB;
 theorems ENUMSET, RELATION, RELAT_AB;

begin

definition
  let R be Relation;
  attr R is Function-like means :def1:
  for x,y,z being set st [x,y] in R & [x,z] in R holds y=z;
end;

theorem l1:
  {} is Function-like
  proof
    let x,y,z be set;
    assume [x,y] in {} & [x,z] in {};
    hence y=z by ENUMSET:def 1;
  end;
  
registration
  cluster Function-like Relation;
  existence by l1;
end;

registration
  cluster {} -> Function-like Relation;
  coherence by l1;
end;

theorem l2:
  for A,B being set holds {} is Relation of A,B
  proof
    let A,B be set;
    thus dom {} c= A
    proof
      let x be set;
      assume x in dom {}; then
      consider y being set such that
      y: [x,y] in {} by RELAT_AB:def 1;
      thus thesis by y,ENUMSET:def 1;
    end;
    thus rng {} c= B
    proof
      let x be set;
      assume x in rng {}; then
      consider y being set such that
      y: [y,x] in {} by RELAT_AB:def 2;
      thus thesis by y,ENUMSET:def 1;
    end;
  end;
  
registration
  let A,B be set;
  cluster Function-like Relation of A,B;
  existence
  proof
    take {};
    thus thesis by l2;
  end;
end;

definition
  mode Function is Function-like Relation;  
end;

registration
  let X be set;
  cluster id X -> Function-like;
  coherence
  proof
    let x,y,z be set;
    assume [x,y] in id X & [x,z] in id X; then
    x=y & x=z by RELAT_AB:def 6;
    hence y=z;
  end;
end;

for X being set holds id X is Function;

definition
  let f be Function;
  let x be set;
  assume x: x in dom f;
  func f.x means :def2:
  [x,it] in f;
  existence by RELAT_AB:def 1,x;
  uniqueness
  proof
    let a,b be set;
    assume [x,a] in f & [x,b] in f;
    hence a=b by def1;
  end;
end;

definition
  let f,g be Function;
  redefine pred f=g means
  dom f = dom g & for x being set st x in dom f holds f.x=g.x;
  compatibility
  proof
    thus f=g implies dom f = dom g & for x being set st x in dom f holds f.x=g.x;
    assume d: (dom f = dom g) &
    (for x being set st x in dom f holds f.x=g.x);
    thus f=g
    proof
      thus f c= g
      proof
        let a,b be set;
        assume a: [a,b] in f; then
        b: a in dom f by RELAT_AB:def 1; then
        b=f.a by def2,a; then
        b=g.a by d,b;
        hence [a,b] in g by b,def2,d;
      end;
      thus g c= f
      proof
        let a,b be set;
        assume a: [a,b] in g; then
        b: a in dom g by RELAT_AB:def 1; then
        b=g.a by def2,a; then
        b=f.a by d,b;
        hence [a,b] in f by b,def2,d;
      end;
    end;
  end;
end;

definition
  let f be Function;
  attr f is one-to-one means :def3:
  for x,y being set st x in dom f & y in dom f & f.x = f.y holds x=y;
end;

notation
  let f be Function;
  synonym f is injective for f is one-to-one;
end;

for f being Function holds f is injective iff f is one-to-one;

theorem l3:
  {} is one-to-one
  proof
    let x,y be set;
    assume x in dom {} & y in dom {} & {}.x={}.y;
    then consider y being set such that
    y: [x,y] in {} by RELAT_AB:def 1;
    thus thesis by y,ENUMSET:def 1;
  end;

registration
  cluster {} -> one-to-one Function;
  coherence by l3;
  cluster one-to-one Function;
  existence
  proof
    take {};
    thus thesis;
  end;
end;

theorem t1:
  for f being one-to-one Function holds f~ is Function
  proof
    let f be one-to-one Function;
    f~ is Function-like
    proof
      let a,b,c be set;
      assume [a,b] in f~ & [a,c] in f~; then
      b: [b,a] in f & [c,a] in f by RELATION:def 3; then
      c: b in dom f & c in dom f by RELAT_AB:def 1; then
      f.b = a & f.c = a by def2,b;
      hence b=c by def3,c;
    end;
    hence f~ is Function-like Relation;
  end;

registration
  let f,g be Function;
  cluster f*g -> Function-like;  
  coherence
  proof
    let x,y,z be set;
    assume a: [x,y] in f*g & [x,z] in f*g;
    consider u being set such that
    u: [x,u] in f & [u,y] in g by a,RELATION:def 7;
    consider v being set such that
    v: [x,v] in f & [v,z] in g by a,RELATION:def 7;
    u = v by def1,u,v;
    hence y=z by def1,u,v;
  end;
end;

theorem t2:
  for f,g being one-to-one Function holds f*g is one-to-one
  proof
    let f,g being one-to-one Function;
    let x,y be set;
    assume a: x in dom (f*g) & y in dom (f*g) & (f*g).x=(f*g).y;
    consider u being set such that
    u: [x,u] in f*g by a,RELAT_AB:def 1;
    consider v being set such that
    v: [y,v] in f*g by a,RELAT_AB:def 1;
    consider z being set such that
    z: [x,z] in f & [z,u] in g by u,RELATION:def 7;
    consider s being set such that
    s: [y,s] in f & [s,v] in g by v,RELATION:def 7;
    uv: u = (f*g).x by a,def2,u
    .= v by a,def2,v;
    zs: z in dom g & s in dom g by RELAT_AB:def 1,z,s; then
    u=g.z & v=g.s by def2,z,s; then
    zes: z=s by def3,zs,uv;
    xy: x in dom f & y in dom f by z,s,RELAT_AB:def 1; then
    f.x = z & f.y = s by z,s,def2;
    hence x=y by def3,xy,zes;
  end;

theorem t3:
  ex f being Function st f is not one-to-one
  proof
    set f = {[1,1],[2,1]};
    reconsider f as Relation by RELATION:2;
    now
      let x,y,z be set;
      assume [x,y] in f & [x,z] in f; then
      ([x,y]=[1,1] or [x,y]=[2,1]) & ([x,z]=[1,1] or [x,z]=[2,1]) by ENUMSET:def 4; then
      (x=1 & y=1 or x=2 & y=1) & (x=1 & z=1 or x=2 & z=1) by ENUMSET:2; 
      hence y = z;
    end; then
    reconsider f as Function by def1;
    take f;
    j: [1,1] in f & [2,1] in f by ENUMSET:def 4; then
    k: 1 in dom f & 2 in dom f by RELAT_AB:def 1; then
    f.1 = 1 by j,def2 .= f.2 by j,k,def2;
    hence thesis by def3,k;
  end;