A1: rng (I `1) c= the carrier of T
proof
let x be object ; :: 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 object such that
A2: a in dom (I `1) and
A3: x = (I `1) . a by FUNCT_1:def 3;
reconsider a = a as Object of C by A2, PARTFUN1:def 2;
(I `1) . a is Object of T by Def9;
hence x in the carrier of T by A3; :: thesis: verum
end;
dom (I `1) = the carrier of C by PARTFUN1:def 2;
then reconsider I1 = I `1 as Function of the carrier of C, the carrier of T by A1, FUNCT_2:def 1, RELSET_1:4;
deffunc H1( Object of C) -> Element of the carrier of T = I1 . $1;
deffunc H2( Morphism of C) -> object = [[((I `1) . (dom $1)),((I `1) . (cod $1))],((I `2) . $1)];
A4: now :: thesis: for f being Morphism of C holds
( H2(f) is Morphism of T & ( for g being Morphism of T st g = H2(f) holds
( dom g = H1( dom f) & cod g = H1( cod f) ) ) )
let f be Morphism of C; :: thesis: ( H2(f) is Morphism of T & ( for g being Morphism of T st g = H2(f) holds
( dom g = H1( dom f) & cod g = H1( cod f) ) ) )
thus H2(f) is Morphism of T by Def9; :: thesis: for g being Morphism of T st g = H2(f) holds
( dom g = H1( dom f) & cod g = H1( cod f) )
let g be Morphism of T; :: thesis: ( g = H2(f) implies ( dom g = H1( dom f) & cod g = H1( cod f) ) )
assume A5: g = H2(f) ; :: thesis: ( dom g = H1( dom f) & cod g = H1( cod f) )
hence dom g = H2(f) `11 by CAT_5:13
.= H1( dom f) by MCART_1:85 ;
:: thesis: cod g = H1( cod f)
thus cod g = H2(f) `12 by A5, CAT_5:13
.= H1( cod f) by MCART_1:85 ; :: thesis: verum
end;
A6: now :: thesis: for f1, f2 being Morphism of C
for g1, g2 being Morphism of T st g1 = H2(f1) & g2 = H2(f2) & dom f2 = cod f1 holds
H2(f2 (*) f1) = g2 (*) g1
let f1, f2 be Morphism of C; :: thesis: for g1, g2 being Morphism of T st g1 = H2(f1) & g2 = H2(f2) & dom f2 = cod f1 holds
H2(f2 (*) f1) = g2 (*) g1
let g1, g2 be Morphism of T; :: thesis: ( g1 = H2(f1) & g2 = H2(f2) & dom f2 = cod f1 implies H2(f2 (*) f1) = g2 (*) g1 )
assume that
A7: ( g1 = H2(f1) & g2 = H2(f2) ) and
A8: dom f2 = cod f1 ; :: thesis: H2(f2 (*) f1) = g2 (*) g1
A9: ( dom (f2 (*) f1) = dom f1 & cod (f2 (*) f1) = cod f2 ) by A8, CAT_1:17;
A10: ( (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;
(I `2) . (f2 (*) f1) = ((I `2) . f2) * ((I `2) . f1) by A8, Th6;
hence H2(f2 (*) f1) = g2 (*) g1 by A7, A8, A10, A9, CAT_5:def 6; :: thesis: verum
end;
A11: now :: thesis: for a being Object of C holds H2( id a) = id H1(a)
let a be Object of C; :: thesis: H2( id a) = id H1(a)
thus H2( id a) = [[(I1 . a),(I1 . a)],(id ((I `1) . a))] by Th6
.= id H1(a) by 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 = H2(f) from CAT_5:sch 3(A4, A11, A6); :: thesis: verum