let C be Cartesian_category; :: thesis: for a being Object of C
for f1, f2 being Morphism of a, [1] C holds f1 = f2
let a be Object of C; :: thesis: for f1, f2 being Morphism of a, [1] C holds f1 = f2
let f1, f2 be Morphism of a, [1] C; :: thesis: f1 = f2
[1] C is terminal by Def8;
then consider f being Morphism of a, [1] C such that
A1: for g being Morphism of a, [1] C holds f = g ;
thus f1 = f by A1
.= f2 by A1 ; :: thesis: verum