proposition: Theorem produit_reel_affixe_vecteur : forall (k : R) (z z' : C) (A B A' B' : PO), z = affixe_vec (vec A B) :>C -> z' = affixe_vec (vec A' B') :>C -> z' = Cmult (Rinj k) z :>C -> vec A' B' = mult_PP k (vec A B) :>PP.
proof: Proof. intros k z z' A B A' B'; try assumption. elim existence_representant_vecteur with (A := O) (B := A) (C := B); intros M; intros H1. elim existence_representant_vecteur with (A := O) (B := A') (C := B'); intros M'; intros H2. rewrite <- H2; rewrite <- H1; intros. apply (produit_reel_affixe_vecteur_OM (k:=k) (z:=z) (z':=z') (M:=M) (M':=M')); auto. Qed.