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₂()

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng F ; :: thesis:
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:

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;

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

end;

let f be Morphism of F₁(); :: thesis:
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:
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:

end;

let f, g be Morphism of F₁(); :: thesis:
assume A10: dom g = cod f ; :: thesis:
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:

end;

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