defpred S1[ object , object ] means for f being Morphism of A st $1 = f holds
$2 = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)];
A1: now :: thesis: for m being object st m in the carrier' of A holds
ex o being object st
( o in the carrier' of (Functors (B,C)) & S1[m,o] )
let m be object ; :: thesis: ( m in the carrier' of A implies ex o being object st
( o in the carrier' of (Functors (B,C)) & S1[m,o] ) )
assume m in the carrier' of A ; :: thesis: ex o being object st
( o in the carrier' of (Functors (B,C)) & S1[m,o] )
then reconsider g = m as Morphism of A ;
reconsider o = [[(F ?- (dom g)),(F ?- (cod g))],(F ?- g)] as object ;
take o = o; :: thesis: ( o in the carrier' of (Functors (B,C)) & S1[m,o] )
F ?- (dom g) is_naturally_transformable_to F ?- (cod g) by Th14;
then o in NatTrans (B,C) by NATTRA_1:32;
hence o in the carrier' of (Functors (B,C)) by NATTRA_1:def 17; :: thesis: S1[m,o]
thus S1[m,o] ; :: thesis: verum
end;
consider G being Function of the carrier' of A, the carrier' of (Functors (B,C)) such that
A2: for m being object st m in the carrier' of A holds
S1[m,G . m] from FUNCT_2:sch 1(A1);
 G is Functor of A, Functors (B,C)
proof
thus for c being Object of A ex d being Object of (Functors (B,C)) st G . (id c) = id d :: according to ISOCAT_1:def 1 :: thesis: ( ( for b1 being Element of the carrier' of A holds
( G . (id (dom b1)) = id (dom (G . b1)) & G . (id (cod b1)) = id (cod (G . b1)) ) ) & ( for b1, b2 being Element of the carrier' of A holds
( not dom b2 = cod b1 or G . (b2 (*) b1) = (G . b2) (*) (G . b1) ) ) )
proof
let c be Object of A; :: thesis: ex d being Object of (Functors (B,C)) st G . (id c) = id d
reconsider d = F ?- c as Object of (Functors (B,C)) by Th5;
take d ; :: thesis: G . (id c) = id d
thus G . (id c) = [[(F ?- c),(F ?- c)],(F ?- (id c))] by A2
.= [[(F ?- c),(F ?- c)],(id (F ?- c))] by Th16
.= id d by NATTRA_1:def 17 ; :: thesis: verum
end;
thus for f being Morphism of A holds
( G . (id (dom f)) = id (dom (G . f)) & G . (id (cod f)) = id (cod (G . f)) ) :: thesis: for b1, b2 being Element of the carrier' of A holds
( not dom b2 = cod b1 or G . (b2 (*) b1) = (G . b2) (*) (G . b1) )
proof
let f be Element of the carrier' of A; :: thesis: ( G . (id (dom f)) = id (dom (G . f)) & G . (id (cod f)) = id (cod (G . f)) )
reconsider d = F ?- (dom f), c = F ?- (cod f) as Object of (Functors (B,C)) by Th5;
A3: G . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] by A2;
thus G . (id (dom f)) = [[(F ?- (dom f)),(F ?- (dom f))],(F ?- (id (dom f)))] by A2
.= [[(F ?- (dom f)),(F ?- (dom f))],(id (F ?- (dom f)))] by Th16
.= id d by NATTRA_1:def 17
.= id (dom (G . f)) by A3, NATTRA_1:33 ; :: thesis: G . (id (cod f)) = id (cod (G . f))
thus G . (id (cod f)) = [[(F ?- (cod f)),(F ?- (cod f))],(F ?- (id (cod f)))] by A2
.= [[(F ?- (cod f)),(F ?- (cod f))],(id (F ?- (cod f)))] by Th16
.= id c by NATTRA_1:def 17
.= id (cod (G . f)) by A3, NATTRA_1:33 ; :: thesis: verum
end;
let f, g be Morphism of A; :: thesis: ( not dom g = cod f or G . (g (*) f) = (G . g) (*) (G . f) )
assume A4: dom g = cod f ; :: thesis: G . (g (*) f) = (G . g) (*) (G . f)
then reconsider t = F ?- f as natural_transformation of F ?- (dom f),F ?- (dom g) ;
A5: ( cod (g (*) f) = cod g & dom (g (*) f) = dom f ) by A4, CAT_1:17;
A6: F ?- (dom g) is_naturally_transformable_to F ?- (cod g) by Th14;
( the carrier' of (Functors (B,C)) = NatTrans (B,C) & F ?- (dom f) is_naturally_transformable_to F ?- (cod f) ) by Th14, NATTRA_1:def 17;
then reconsider gg = [[(F ?- (dom g)),(F ?- (cod g))],(F ?- g)], ff = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] as Morphism of (Functors (B,C)) by A6, NATTRA_1:32;
A7: G . f = ff by A2;
thus G . (g (*) f) = [[(F ?- (dom (g (*) f))),(F ?- (cod (g (*) f)))],(F ?- (g (*) f))] by A2
.= [[(F ?- (dom (g (*) f))),(F ?- (cod (g (*) f)))],((F ?- g) `*` t)] by A4, Th17
.= gg (*) ff by A4, A5, NATTRA_1:36
.= (G . g) (*) (G . f) by A2, A7 ; :: thesis: verum
end;
then reconsider G = G as Functor of A, Functors (B,C) ;
take G ; :: thesis: for f being Morphism of A holds G . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)]
thus for f being Morphism of A holds G . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] by A2; :: thesis: verum