environ vocabularies RELAT_1, XBOOLE_0, FUNCT_1; notations TARSKI, XBOOLE_0, RELAT_1, FUNCT_1; constructors TARSKI, XBOOLE_0, FUNCT_1; registrations XBOOLE_0, RELAT_1; definitions FUNCT_1; theorems XBOOLE_0, RELAT_1, FUNCT_1; begin reserve x,x1,x2,y,y1,y2,z1,z2 for set; reserve f,g for Function; theorem Th1: g*f is Function-like proof let x,y1,y2; assume [x,y1] in g*f; then consider z1 such that A1: [x,z1] in f and A2: [z1,y1] in g by RELAT_1:def 8; assume [x,y2] in g*f; then consider z2 such that A3: [x,z2] in f and A4: [z2,y2] in g by RELAT_1:def 8; z1 = z2 by A1,A3,FUNCT_1:def 1; hence thesis by A2,A4,FUNCT_1:def 1; end; registration let f,g be Function; cluster g*f -> Function-like; correctness by Th1; end; theorem Th2: f is one-to-one & g is one-to-one implies g*f is one-to-one proof assume that A1: f is one-to-one and A2: g is one-to-one; let x1,x2; assume A3: x1 in dom(g*f) & x2 in dom(g*f); then A4: (g*f).x1 = g.(f.x1) & (g*f).x2 = g .(f.x2) by FUNCT_1:22; A5: x1 in dom f & x2 in dom f by A3,FUNCT_1:21; assume A6: (g*f).x1 = (g*f).x2; f.x1 in dom g & f.x2 in dom g by A3,FUNCT_1:21; then f.x1 = f.x2 by A2,A4,A6,FUNCT_1:def 8; hence x1 = x2 by A1,A5,FUNCT_1:def 8; end; registration cluster empty -> Function-like set; coherence proof let f be set; assume A1: f is empty; let x,y1,y2; thus thesis by A1,XBOOLE_0:def 1; end; end; registration cluster empty -> one-to-one Function; coherence proof let f be Function; assume A1: f is empty; let x1,x2; thus thesis by A1,XBOOLE_0:def 1; end; end; registration cluster one-to-one Function; existence proof take {}; thus thesis; end; end; registration let f,g be one-to-one Function; cluster g*f -> one-to-one; coherence by Th2; end;