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

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

end;

hence l | (Seg n) is LeftLinearCombination of A by Def9; :: thesis: verum