proposition: Lemma ext_map_prod_compose I p1 p2 p3 g f h: ext_map_prod_axioms I p1 p2 f -> ext_map_prod_axioms I p2 p3 g -> (forall i, inc i I -> h i = (g i) \cf (f i)) -> (forall i, inc i I -> (g i) \cfP (f i)) -> (ext_map_prod I p2 p3 g) \co (ext_map_prod I p1 p2 f) = (ext_map_prod I p1 p3 h).
proof: Proof. move=> emp1 emp2 alh alfc. set f1:= (ext_map_prod I p2 p3 g). set f2:= (ext_map_prod I p1 p2 f). set f3:= (ext_map_prod I p1 p3 h). move: (ext_map_prod_composable emp1 emp2 alh alfc) => emp3. have cee: (f1 \coP f2). split; first by apply: ext_map_prod_f. by apply: ext_map_prod_f. by rewrite /f1/f2/ext_map_prod; aw. have fcee: (function (f1 \co f2)) by fct_tac. have sf23: source f2 = source f3. by rewrite /f2 /f3/ext_map_prod; aw. have tf13: target f1 = target f3. by rewrite /f1 /f3/ext_map_prod; aw. apply: function_exten; aw => //. by apply: ext_map_prod_f =>//. move=> x xs; rewrite compfV //. have xp: inc x (productf I p1) by move: xs; rewrite /f2/ext_map_prod; aw. set t:= Vf f2 x. have tv: t = Lg I (ext_map_prod_aux x f) by rewrite /t/f2 ext_map_prod_V //. have ->: (Vf f1 t = Lg I (ext_map_prod_aux t g)). rewrite /f1 ext_map_prod_V //. have tf2: (target f2 = productf I p2) by rewrite/f2/ext_map_prod; aw. rewrite/t -tf2; Wtac. by rewrite/f2; apply: ext_map_prod_f =>//. have ->: Vf f3 x = Lg I (ext_map_prod_aux x h) by rewrite/f3 ext_map_prod_V. apply: Lg_exten => e ei; rewrite tv /ext_map_prod_aux. rewrite LgV //. have aux:= (alfc _ ei). rewrite (alh _ ei) composef_ev // (proj32 (emp1 _ ei)). by move /setXf_P: xp => [_ dx]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)