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:35;
hence o in the carrier' of (Functors B,C) by NATTRA_1:def 18; :: 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:44;
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 18 ;
:: 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: ( dom (id (dom f)) = dom f & cod (id (dom f)) = dom f & dom (id (cod f)) = cod f & cod (id (cod f)) = cod f ) by CAT_1:44;
A4: 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, A3
.= [[(F ?- (dom f)),(F ?- (dom f))],(id (F ?- (dom f)))] by Th20
.= id d by NATTRA_1:def 18
.= id (dom (G . f)) by A4, NATTRA_1:39 ; :: 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, A3
.= [[(F ?- (cod f)),(F ?- (cod f))],(id (F ?- (cod f)))] by Th20
.= id c by NATTRA_1:def 18
.= id (cod (G . f)) by A4, NATTRA_1:39 ; :: 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 A5: 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) ;
( the carrier' of (Functors B,C) = NatTrans B,C & F ?- (dom f) is_naturally_transformable_to F ?- (cod f) & F ?- (dom g) is_naturally_transformable_to F ?- (cod g) ) by Th18, NATTRA_1:def 18;
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 NATTRA_1:35;
A6: ( cod (g * f) = cod g & dom (g * f) = dom f ) by A5, CAT_1:42;
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 A5, Th21
.= gg * ff by A5, A6, NATTRA_1:42
.= (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