let f be XFinSequence of ; :: 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 C1: i in len f by NAT_1:45;
( dom (f + a) = dom f & ( for c being set st c in dom (f + a) holds
(f + a) . c = a + (f . c) ) ) by VALUED_1:def 2;
hence (f + a) . i = (f . i) + a by C1; :: thesis: verum