let C1, C2 be non empty AltGraph ; :: thesis: for F being Covariant FunctorStr of 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 of 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 Def13;
then consider f being Function of the carrier of C1,the carrier of C2 such that
A1: the ObjectMap of F = [:f,f:] by Def2;
A2: F . o1 = [(f . o1),(f . o1)] `1 by A1, FUNCT_3:96
.= f . o1 by MCART_1:7 ;
F . o2 = [(f . o2),(f . o2)] `1 by A1, FUNCT_3:96
.= f . o2 by MCART_1:7 ;
hence the ObjectMap of F . o1,o2 = [(F . o1),(F . o2)] by A1, A2, FUNCT_3:96; :: thesis: verum