+definition induced_norm_fun ≝
+ λR:real.λV:integration_riesz_space R.λf:V.
+ integral ? V (absolute_value ? ? f).
+
+lemma induced_norm_is_norm:
+ ∀R:real.∀V:integration_riesz_space R.is_norm R V (induced_norm_fun ? V).
+ elim daemon.(*
+ intros;
+ apply mk_is_norm;
+ [ apply mk_is_semi_norm;
+ [ unfold induced_norm_fun;
+ intros;
+ apply positive;
+ [ apply (irs_positive_linear ? V)
+ | (* difficile *)
+ elim daemon
+ ]
+ | intros;
+ unfold induced_norm_fun;
+ (* facile *)
+ elim daemon
+ | intros;
+ unfold induced_norm_fun;
+ (* difficile *)
+ elim daemon
+ ]
+ | intros;
+ unfold induced_norm_fun in H;
+ apply irs_quotient_space1;
+ unfold minus;
+ rewrite < plus_comm;
+ rewrite < eq_zero_opp_zero;
+ rewrite > zero_neutral;
+ assumption
+ ].*)
+qed.
+
+definition induced_norm ≝
+ λR:real.λV:integration_riesz_space R.
+ mk_norm ? ? (induced_norm_fun ? V) (induced_norm_is_norm ? V).
+
+lemma is_riesz_norm_induced_norm:
+ ∀R:real.∀V:integration_riesz_space R.
+ is_riesz_norm ? ? (induced_norm ? V).
+ intros;
+ unfold is_riesz_norm;
+ intros;
+ unfold induced_norm;
+ simplify;
+ unfold induced_norm_fun;
+ (* difficile *)
+ elim daemon.
+qed.
+
+definition induced_riesz_norm ≝
+ λR:real.λV:integration_riesz_space R.
+ mk_riesz_norm ? ? (induced_norm ? V) (is_riesz_norm_induced_norm ? V).
+
+definition distance_induced_by_integral ≝
+ λR:real.λV:integration_riesz_space R.
+ induced_distance ? ? (induced_norm R V).
+
+definition is_complete_integration_riesz_space ≝
+ λR:real.λV:integration_riesz_space R.
+ is_complete ? ? (distance_induced_by_integral ? V).
+
+record complete_integration_riesz_space (R:real) : Type ≝
+ { cirz_integration_riesz_space:> integration_riesz_space R;
+ cirz_complete_integration_riesz_space_property:
+ is_complete_integration_riesz_space ? cirz_integration_riesz_space
+ }.
+
+(* now we prove that any complete integration riesz space is an L-space *)
+
+(*theorem is_l_space_l_space_induced_by_integral:
+ ∀R:real.∀V:complete_integration_riesz_space R.
+ is_l_space ? ? (induced_riesz_norm ? V).
+ intros;
+ constructor 1;
+ [ apply cirz_complete_integration_riesz_space_property
+ | intros;
+ unfold induced_riesz_norm;
+ simplify;
+ unfold induced_norm;
+ simplify;
+ unfold induced_norm_fun;
+ (* difficile *)
+ elim daemon
+ ].
+qed.*)
+
+(**************************** f-ALGEBRAS ********************************)
+