let f be XFinSequence of REAL ; :: thesis: for a being Element of REAL holds
( len (f + a) = len f & ( for i being Nat st i < len f holds
(f + a) . i = (f . i) + a ) )
let a be Element of REAL ; :: thesis: ( len (f + a) = len f & ( for i being Nat st i < len f holds
(f + a) . i = (f . i) + a ) )
thus len (f + a) = len f by VALUED_1:def 2; :: thesis: for i being Nat st i < len f holds
(f + a) . i = (f . i) + a
let i be Nat; :: thesis: ( i < len f implies (f + a) . i = (f . i) + a )
assume i < len f ; :: thesis: (f + a) . i = (f . i) + a
then A1: i in len f by NAT_1:45;
dom (f + a) = dom f by VALUED_1:def 2;
hence (f + a) . i = (f . i) + a by A1, VALUED_1:def 2; :: thesis: verum