let f, g be Function; :: thesis: ( f is one-to-one implies for x being object st x in dom f holds
Coim ((f * g),(f . x)) = Coim (g,x) )
assume A1: f is one-to-one ; :: thesis: for x being object st x in dom f holds
Coim ((f * g),(f . x)) = Coim (g,x)
let x be object ; :: thesis: ( x in dom f implies Coim ((f * g),(f . x)) = Coim (g,x) )
assume A2: x in dom f ; :: thesis: Coim ((f * g),(f . x)) = Coim (g,x)
set fg = f * g;
thus Coim ((f * g),(f . x)) c= Coim (g,x) :: according to XBOOLE_0:def 10 :: thesis: Coim (g,x) c= Coim ((f * g),(f . x))

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Coim ((f * g),(f . x)) or z in Coim (g,x) )
assume A3: z in Coim ((f * g),(f . x)) ; :: thesis: z in Coim (g,x)
then A4: z in dom (f * g) by FUNCT_1:def 7;
A5: (f * g) . z in {(f . x)} by A3, FUNCT_1:def 7;
A6: z in dom g by A4, FUNCT_1:11;
A7: g . z in dom f by A4, FUNCT_1:11;
A8: (f * g) . z = f . (g . z) by A4, FUNCT_1:12;
(f * g) . z = f . x by A5, TARSKI:def 1;
then g . z = x by A7, A8, A2, A1;
then g . z in {x} by TARSKI:def 1;
hence z in Coim (g,x) by FUNCT_1:def 7, A6; :: thesis: verum

end;

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Coim (g,x) or z in Coim ((f * g),(f . x)) )
assume A9: z in Coim (g,x) ; :: thesis: z in Coim ((f * g),(f . x))
then A10: z in dom g by FUNCT_1:def 7;
g . z in {x} by A9, FUNCT_1:def 7;
then A11: g . z = x by TARSKI:def 1;
then A12: (f * g) . z = f . x by FUNCT_1:13, A10;
A13: z in dom (f * g) by A11, A2, FUNCT_1:11, A10;
f . x in {(f . x)} by TARSKI:def 1;
hence z in Coim ((f * g),(f . x)) by A12, A13, FUNCT_1:def 7; :: thesis: verum