let R be non empty multLoopStr ; 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; for l being LinearCombination of A
for n being Nat holds l | (Seg n) is LinearCombination of A
let l be LinearCombination of A; for n being Nat holds l | (Seg n) is LinearCombination of A
let n be Nat; l | (Seg n) is LinearCombination of A
reconsider ln = l | (Seg n) as FinSequence of the carrier of R by FINSEQ_1:18;
now 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) * vlet i be
set ;
( 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
;
ex u, v being Element of R ex a being Element of A st ln /. i = (u * a) * vA2:
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;
ex v being Element of R ex a being Element of A st ln /. i = (u * a) * vtake v =
v;
ex a being Element of A st ln /. i = (u * a) * vtake a =
a;
ln /. i = (u * a) * vthus 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
;
verum end;
hence
l | (Seg n) is LinearCombination of A
by Def8; verum