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 :: thesis: for f being Morphism of A holds G1 . f = G2 . f
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:63; :: thesis: verum