consider F being Function such that
A4: dom F = the carrier' of F₁() and
A5: for x being object st x in the carrier' of F₁() holds
F . x = F₄(x) from FUNCT_1:sch 3();
rng F c= the carrier' of F₂()

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F or x in the carrier' of F₂() )
assume x in rng F ; :: thesis: x in the carrier' of F₂()
then consider y being object such that
A6: y in dom F and
A7: x = F . y by FUNCT_1:def 3;
x = F₄(y) by A4, A5, A6, A7;
then x is Morphism of F₂() by A1, A4, A6;
hence x in the carrier' of F₂() ; :: thesis: verum

end;

then reconsider F = F as Function of the carrier' of F₁(), the carrier' of F₂() by A4, FUNCT_2:def 1, RELSET_1:4;

A8: now :: thesis: for c being Object of F₁() ex d being Object of F₂() st F . (id c) = id d

let c be Object of F₁(); :: thesis: ex d being Object of F₂() st F . (id c) = id d
take d = F₃(c); :: thesis: F . (id c) = id d
thus F . (id c) = F₄((id c)) by A5
.= id d by A2 ; :: thesis: verum

end;

A9: now :: thesis: for f being Morphism of F₁() holds
( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) )

let f be Morphism of F₁(); :: thesis: ( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) )
reconsider g = F₄(f) as Morphism of F₂() by A1;
thus F . (id (dom f)) = F₄((id (dom f))) by A5
.= id F₃((dom f)) by A2
.= id (dom g) by A1
.= id (dom (F . f)) by A5 ; :: thesis: F . (id (cod f)) = id (cod (F . f))
thus F . (id (cod f)) = F₄((id (cod f))) by A5
.= id F₃((cod f)) by A2
.= id (cod g) by A1
.= id (cod (F . f)) by A5 ; :: thesis: verum

end;

now :: thesis: for f, g being Morphism of F₁() st dom g = cod f holds
F . (g (*) f) = (F . g) (*) (F . f)

let f, g be Morphism of F₁(); :: thesis: ( dom g = cod f implies F . (g (*) f) = (F . g) (*) (F . f) )
assume A10: dom g = cod f ; :: thesis: F . (g (*) f) = (F . g) (*) (F . f)
A11: F . g = F₄(g) by A5;
A12: F . f = F₄(f) by A5;
F . (g (*) f) = F₄((g (*) f)) by A5;
hence F . (g (*) f) = (F . g) (*) (F . f) by A3, A10, A11, A12; :: thesis: verum

end;

then reconsider F = F as Functor of F₁(),F₂() by A8, A9, CAT_1:61;
take F ; :: thesis: for f being Morphism of F₁() holds F . f = F₄(f)
thus for f being Morphism of F₁() holds F . f = F₄(f) by A5; :: thesis: verum