let G1, G2 be Functor of A, Functors B,C; :: thesis: ( ( for f being Morphism of A holds G1 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] ) & ( for f being Morphism of A holds G2 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] ) implies G1 = G2 )
assume that
A8: for f being Morphism of A holds G1 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] and
A9: for f being Morphism of A holds G2 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] ; :: thesis: G1 = G2

now

let f be Morphism of A; :: thesis: G1 . f = G2 . f
thus G1 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] by A8
.= G2 . f by A9 ; :: thesis: verum

end;

hence G1 = G2 by FUNCT_2:113; :: thesis: verum