let a be Real; :: thesis: for X being RealUnitarySpace
for seq1 being sequence of X st seq1 is constant holds
a * seq1 is constant
let X be RealUnitarySpace; :: thesis: for seq1 being sequence of X st seq1 is constant holds
a * seq1 is constant
let seq1 be sequence of X; :: thesis: ( seq1 is constant implies a * seq1 is constant )
assume A1: seq1 is constant ; :: thesis: a * seq1 is constant
set seq = a * seq1;
consider x being Point of X such that
A3: for n being Nat holds seq1 . n = x by A1, VALUED_0:def 18;
take z = a * x; :: according to VALUED_0:def 20 :: thesis: for b₁ being set holds (a * seq1) . b₁ = z
let n be Nat; :: thesis: (a * seq1) . n = z
n in NAT by ORDINAL1:def 12;
hence (a * seq1) . n = a * (seq1 . n) by NORMSP_1:def 5
.= z by A3 ;
:: thesis: verum