defpred S₁[ set , set ] means for f being Morphism of A st $1 = f holds
$2 = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)];

A1: now

let m be set ; :: thesis: ( m in the carrier' of A implies ex o being set st
( o in the carrier' of (Functors (B,C)) & S₁[m,o] ) )
assume m in the carrier' of A ; :: thesis: ex o being set st
( o in the carrier' of (Functors (B,C)) & S₁[m,o] )
then reconsider g = m as Morphism of A ;
take o = [[(F ?- (dom g)),(F ?- (cod g))],(F ?- g)]; :: thesis: ( o in the carrier' of (Functors (B,C)) & S₁[m,o] )
F ?- (dom g) is_naturally_transformable_to F ?- (cod g) by Th18;
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: S₁[m,o]
thus S₁[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 set st m in the carrier' of A holds
S₁[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 b₁ being Element of the carrier' of A holds
( G . (id (dom b₁)) = id (dom (G . b₁)) & G . (id (cod b₁)) = id (cod (G . b₁)) ) ) & ( for b₁, b₂ being Element of the carrier' of A holds
( not dom b₂ = cod b₁ or G . (b₂ * b₁) = (G . b₂) * (G . b₁) ) ) )

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 Th8;
take d ; :: thesis: G . (id c) = id d
( dom (id c) = c & cod (id c) = c ) by CAT_1:19;
hence G . (id c) = [[(F ?- c),(F ?- c)],(F ?- (id c))] by A2
.= [[(F ?- c),(F ?- c)],(id (F ?- c))] by Th20
.= 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 b₁, b₂ being Element of the carrier' of A holds
( not dom b₂ = cod b₁ or G . (b₂ * b₁) = (G . b₂) * (G . b₁) )

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 Th8;
A3: G . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] by A2;
( dom (id (dom f)) = dom f & cod (id (dom f)) = dom f ) by CAT_1:19;
hence 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 Th20
.= 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))
( dom (id (cod f)) = cod f & cod (id (cod f)) = cod f ) by CAT_1:19;
hence 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 Th20
.= 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 Th18;
( the carrier' of (Functors (B,C)) = NatTrans (B,C) & F ?- (dom f) is_naturally_transformable_to F ?- (cod f) ) by Th18, 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, Th21
.= 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