let C1, C2 be non empty AltGraph ; :: thesis: for F being Covariant FunctorStr over C1,C2
for o1, o2 being Object of C1 holds the ObjectMap of F . (o1,o2) = [(F . o1),(F . o2)]
let F be Covariant FunctorStr over C1,C2; :: thesis: for o1, o2 being Object of C1 holds the ObjectMap of F . (o1,o2) = [(F . o1),(F . o2)]
let o1, o2 be Object of C1; :: thesis: the ObjectMap of F . (o1,o2) = [(F . o1),(F . o2)]
the ObjectMap of F is Covariant by Def12;
then consider f being Function of the carrier of C1, the carrier of C2 such that
A1: the ObjectMap of F = [:f,f:] ;
A2: F . o1 = [(f . o1),(f . o1)] `1 by A1, FUNCT_3:75
.= f . o1 ;
F . o2 = [(f . o2),(f . o2)] `1 by A1, FUNCT_3:75
.= f . o2 ;
hence the ObjectMap of F . (o1,o2) = [(F . o1),(F . o2)] by A1, A2, FUNCT_3:75; :: thesis: verum