reconsider T = pr1 ( the carrier' of C, the carrier' of D) as Function of the carrier' of [:C,D:], the carrier' of C ;
now :: thesis: ( ( for cd being Object of [:C,D:] ex c being Object of C st T . (id cd) = id c ) & ( for fg being Morphism of [:C,D:] holds
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for fg, fg9 being Morphism of [:C,D:] st dom fg9 = cod fg holds
T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) ) )
thus for cd being Object of [:C,D:] ex c being Object of C st T . (id cd) = id c :: thesis: ( ( for fg being Morphism of [:C,D:] holds
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for fg, fg9 being Morphism of [:C,D:] st dom fg9 = cod fg holds
T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) ) )
proof
let cd be Object of [:C,D:]; :: thesis: ex c being Object of C st T . (id cd) = id c
consider c being Object of C, d being Object of D such that
A1: cd = [c,d] by DOMAIN_1:1;
A2: T . ((id c),(id d)) = id c by FUNCT_3:def 4;
id cd = [(id c),(id d)] by A1, Th25;
hence ex c being Object of C st T . (id cd) = id c by A2; :: thesis: verum
end;
thus for fg being Morphism of [:C,D:] holds
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) :: thesis: for fg, fg9 being Morphism of [:C,D:] st dom fg9 = cod fg holds
T . (fg9 (*) fg) = (T . fg9) (*) (T . fg)
proof
let fg be Morphism of [:C,D:]; :: thesis: ( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) )
consider f being Morphism of C, g being Morphism of D such that
A3: fg = [f,g] by DOMAIN_1:1;
T . (f,g) = T . fg by A3;
then A4: T . fg = f by FUNCT_3:def 4;
dom [f,g] = [(dom f),(dom g)] by Th22;
hence T . (id (dom fg)) = T . ((id (dom f)),(id (dom g))) by A3, Th25
.= id (dom (T . fg)) by A4, FUNCT_3:def 4 ;
:: thesis: T . (id (cod fg)) = id (cod (T . fg))
cod [f,g] = [(cod f),(cod g)] by Th22;
hence T . (id (cod fg)) = T . ((id (cod f)),(id (cod g))) by A3, Th25
.= id (cod (T . fg)) by A4, FUNCT_3:def 4 ;
:: thesis: verum
end;
let fg, fg9 be Morphism of [:C,D:]; :: thesis: ( dom fg9 = cod fg implies T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) )
assume A5: dom fg9 = cod fg ; :: thesis: T . (fg9 (*) fg) = (T . fg9) (*) (T . fg)
consider f being Morphism of C, g being Morphism of D such that
A6: fg = [f,g] by DOMAIN_1:1;
T . (f,g) = T . fg by A6;
then A7: T . fg = f by FUNCT_3:def 4;
consider f9 being Morphism of C, g9 being Morphism of D such that
A8: fg9 = [f9,g9] by DOMAIN_1:1;
T . (f9,g9) = T . fg9 by A8;
then A9: T . fg9 = f9 by FUNCT_3:def 4;
( dom [f9,g9] = [(dom f9),(dom g9)] & cod [f,g] = [(cod f),(cod g)] ) by Th22;
then ( dom f9 = cod f & dom g9 = cod g ) by A5, A6, A8, XTUPLE_0:1;
hence T . (fg9 (*) fg) = T . ((f9 (*) f),(g9 (*) g)) by A6, A8, Th23
.= (T . fg9) (*) (T . fg) by A9, A7, FUNCT_3:def 4 ;
:: thesis: verum
end;
hence pr1 ( the carrier' of C, the carrier' of D) is Functor of [:C,D:],C by CAT_1:61; :: thesis: verum