let R be non empty multLoopStr ; :: thesis: for A being non empty Subset of R
for l being RightLinearCombination of A
for n being Nat holds l | (Seg n) is RightLinearCombination of A
let A be non empty Subset of R; :: thesis: for l being RightLinearCombination of A
for n being Nat holds l | (Seg n) is RightLinearCombination of A
let l be RightLinearCombination of A; :: thesis: for n being Nat holds l | (Seg n) is RightLinearCombination of A
let n be Nat; :: thesis: l | (Seg n) is RightLinearCombination of A
reconsider ln = l | (Seg n) as FinSequence of the carrier of R by FINSEQ_1:18;

now :: thesis: for i being set st i in dom ln holds
ex v being Element of R ex a being Element of A st ln /. i = a * v

let i be set ; :: thesis: ( i in dom ln implies ex v being Element of R ex a being Element of A st ln /. i = a * v )
assume A1: i in dom ln ; :: thesis: ex v being Element of R ex a being Element of A st ln /. i = a * v
A2: dom ln c= dom l by RELAT_1:60;
then consider v being Element of R, a being Element of A such that
A3: l /. i = a * v by A1, Def10;
take v = v; :: thesis: ex a being Element of A st ln /. i = a * v
take a = a; :: thesis: ln /. i = a * v
thus ln /. i = ln . i by A1, PARTFUN1:def 6
.= l . i by A1, FUNCT_1:47
.= a * v by A1, A2, A3, PARTFUN1:def 6 ; :: thesis: verum

end;

hence l | (Seg n) is RightLinearCombination of A by Def10; :: thesis: verum