let R be non empty multLoopStr ; :: thesis: for A being non empty Subset of R
for l being LinearCombination of A
for n being Nat holds l | (Seg n) is LinearCombination of A
let A be non empty Subset of R; :: thesis: for l being LinearCombination of A
for n being Nat holds l | (Seg n) is LinearCombination of A
let l be LinearCombination of A; :: thesis: for n being Nat holds l | (Seg n) is LinearCombination of A
let n be Nat; :: thesis: l | (Seg n) is LinearCombination 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 u, v being Element of R ex a being Element of A st ln /. i = (u * a) * v

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

end;

hence l | (Seg n) is LinearCombination of A by Def8; :: thesis: verum