proposition: Lemma prl_r2_sf_prop4 (lf:= (projective_limit prl_r2_sf)) (ls:= (projective_limit S)) (u1 := projective_map S u F) (u2 := projective_limit_fun prl_r2_sf S u): [/\ function_prop u2 lf ls, function_prop u1 F ls & forall x, inc x F -> Vf u1 x = Vf u2 (cst_graph (psI S) x)].
proof: Proof. have si: prl_same_index prl_r2_sf S by []. have pa:=(prl_map2_prop si prl_r2_sf_prop3). have pb: prl_map_property S u F u1 by apply: prl_map_prop. split; [ by case: pa | by case: pb | move => x xF]. move:(prl_map_ax compat) => ax1. have pc:inc (cst_graph (psI S) x) (projective_limit prl_r2_sf). rewrite prl_r2_sf_prop2; apply/Zo_P; split. by apply: gfunctions_i1. by rewrite /cst_graph;split; fprops; aw => a b aI bI; rewrite !LgV. have ax2 := (prl_map_ax (prl_map2_prop1 si prl_r2_sf_prop3)). rewrite /u1 /u2 /projective_limit_fun /projective_map !LfV//. apply:Lg_exten => i iI /=. move:(compat) => [_ p2 p3 _]; rewrite p2 in p3. move:(p3 _ iI) =>[fui sui tui]. rewrite prl_map2_prop2 //= LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)