[STATEMENT]
lemma f_carrier[dest]: "i < m \<Longrightarrow> fs ! i \<in> carrier_vec n"
  and fs_carrier [simp]: "set fs \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i < length fs \<Longrightarrow> fs ! i \<in> carrier_vec n) &&& set fs \<subseteq> carrier_vec n
[PROOF STEP]
using lin_indep gs.f_carrier gs.gso_carrier
[PROOF STATE]
proof (prove)
using this:
gs.lin_indpt_list (map of_int_hom.vec_hom fs)
?i < length (map of_int_hom.vec_hom fs) \<Longrightarrow> map of_int_hom.vec_hom fs ! ?i \<in> carrier_vec n
?i < length (map of_int_hom.vec_hom fs) \<Longrightarrow> gs.gso ?i \<in> carrier_vec n

goal (1 subgoal):
 1. (i < length fs \<Longrightarrow> fs ! i \<in> carrier_vec n) &&& set fs \<subseteq> carrier_vec n
[PROOF STEP]
unfolding gs.lin_indpt_list_def
[PROOF STATE]
proof (prove)
using this:
set (map of_int_hom.vec_hom fs) \<subseteq> carrier_vec n \<and> distinct (map of_int_hom.vec_hom fs) \<and> gs.lin_indpt (set (map of_int_hom.vec_hom fs))
?i < length (map of_int_hom.vec_hom fs) \<Longrightarrow> map of_int_hom.vec_hom fs ! ?i \<in> carrier_vec n
?i < length (map of_int_hom.vec_hom fs) \<Longrightarrow> gs.gso ?i \<in> carrier_vec n

goal (1 subgoal):
 1. (i < length fs \<Longrightarrow> fs ! i \<in> carrier_vec n) &&& set fs \<subseteq> carrier_vec n
[PROOF STEP]
by auto