let f, g be Function; ( 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
; for x being object st x in dom f holds
Coim ((f * g),(f . x)) = Coim (g,x)
let x be object ; ( x in dom f implies Coim ((f * g),(f . x)) = Coim (g,x) )
assume A2:
x in dom f
; Coim ((f * g),(f . x)) = Coim (g,x)
set fg = f * g;
thus
Coim ((f * g),(f . x)) c= Coim (g,x)
XBOOLE_0:def 10 Coim (g,x) c= Coim ((f * g),(f . x))proof
let z be
object ;
TARSKI:def 3 ( not z in Coim ((f * g),(f . x)) or z in Coim (g,x) )
assume A3:
z in Coim (
(f * g),
(f . x))
;
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;
verum
end;
let z be object ; TARSKI:def 3 ( not z in Coim (g,x) or z in Coim ((f * g),(f . x)) )
assume A9:
z in Coim (g,x)
; 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; verum