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;