proposition: Lemma egalite_vecteur_image : forall (z z' : C) (A B A' B' : PO), z = affixe_vec (vec A B) :>C -> z' = affixe_vec (vec A' B') :>C -> vec A B = vec A' B' :>PP -> z = z' :>C.
proof: Proof. intros. elim existence_representant_vecteur with (A := O) (B := A) (C := B); intros D H2; intros; try exact H2. elim existence_representant_vecteur with (A := O) (B := A') (C := B'); intros D'; intros; try exact H2. apply egalite_vecteur_OM_image with (M := D) (M' := D'). rewrite H2; auto. rewrite H3; auto. rewrite H2; rewrite H3; auto. Qed.