:: deftheorem Def24 defines F_idxseq LMODFREE:def 24 :
for X being non empty set
for R being non degenerated Ring
for f being Element of (Free_LMod (X,R))
for b₄ being FinSequence of the carrier of (Free_LMod (X,R)) holds
( b₄ = F_idxseq f iff ( len b₄ = len (idxseq f) & ( for i being Nat st i in dom b₄ holds
b₄ . i = (ev_iota f) . ((idxseq f) . i) ) ) );