A1: dom (I `1 ) = the carrier of C by PARTFUN1:def 4;
rng (I `1 ) c= the carrier of T

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (I `1 ) or x in the carrier of T )
assume x in rng (I `1 ) ; :: thesis: x in the carrier of T
then consider a being set such that
A2: ( a in dom (I `1 ) & x = (I `1 ) . a ) by FUNCT_1:def 5;
reconsider a = a as Object of C by A2, PARTFUN1:def 4;
(I `1 ) . a is Object of T by Def9;
hence x in the carrier of T by A2; :: thesis: verum

end;

then reconsider I1 = I `1 as Function of the carrier of C,the carrier of T by A1, FUNCT_2:def 1, RELSET_1:11;
deffunc H<sub>1</sub>( Morphism of C) -> set = [[((I `1 ) . (dom $1)),((I `1 ) . (cod $1))],((I `2 ) . $1)];
deffunc H₂( Object of C) -> Element of the carrier of T = I1 . $1;

A3: now

let f be Morphism of C; :: thesis: ( H₁(f) is Morphism of T & ( for g being Morphism of T st g = H₁(f) holds
( dom g = H₂( dom f) & cod g = H₂( cod f) ) ) )
thus H₁(f) is Morphism of T by Def9; :: thesis: for g being Morphism of T st g = H₁(f) holds
( dom g = H₂( dom f) & cod g = H₂( cod f) )
let g be Morphism of T; :: thesis: ( g = H₁(f) implies ( dom g = H₂( dom f) & cod g = H₂( cod f) ) )
assume A4: g = H₁(f) ; :: thesis: ( dom g = H₂( dom f) & cod g = H₂( cod f) )
hence dom g = H₁(f) `11 by CAT_5:13
.= H<sub>2</sub>( dom f) by MCART_1:89 ;
:: thesis: cod g = H<sub>2</sub>( cod f)
thus cod g = H<sub>1</sub>(f) `12 by A4, CAT_5:13
.= H₂( cod f) by MCART_1:89 ; :: thesis: verum

end;

A5: now

let a be Object of C; :: thesis: H₁( id a) = id H₂(a)
( dom (id a) = a & cod (id a) = a ) by CAT_1:44;
hence H₁( id a) = [[(I1 . a),(I1 . a)],(id ((I `1 ) . a))] by Th6
.= id H₂(a) by CAT_5:def 6 ;
:: thesis: verum

end;

A6: now

let f1, f2 be Morphism of C; :: thesis: for g1, g2 being Morphism of T st g1 = H₁(f1) & g2 = H₁(f2) & dom f2 = cod f1 holds
H₁(f2 * f1) = g2 * g1
let g1, g2 be Morphism of T; :: thesis: ( g1 = H₁(f1) & g2 = H₁(f2) & dom f2 = cod f1 implies H₁(f2 * f1) = g2 * g1 )
assume A7: ( g1 = H₁(f1) & g2 = H₁(f2) & dom f2 = cod f1 ) ; :: thesis: H₁(f2 * f1) = g2 * g1
A8: ( (I `2 ) . f1 is Functor of (I `1 ) . (dom f1),(I `1 ) . (cod f1) & (I `2 ) . f2 is Functor of (I `1 ) . (dom f2),(I `1 ) . (cod f2) ) by Th4;
( dom (f2 * f1) = dom f1 & cod (f2 * f1) = cod f2 & (I `2 ) . (f2 * f1) = ((I `2 ) . f2) * ((I `2 ) . f1) ) by A7, Th6, CAT_1:42;
hence H₁(f2 * f1) = g2 * g1 by A7, A8, CAT_5:def 6; :: thesis: verum

end;

thus ex F being Functor of C,T st
for f being Morphism of C holds F . f = H₁(f) from CAT_5:sch 3(A3, A5, A6); :: thesis: verum