let n be Element of NAT ; :: thesis: for x being Element of REAL n
for f, g being FinSequence of REAL
for r being Real st f = x & g = r * x holds
( len f = len g & ( for i being Element of NAT st 1 <= i & i <= len f holds
g /. i = r * (f /. i) ) )
let x be Element of REAL n; :: thesis: for f, g being FinSequence of REAL
for r being Real st f = x & g = r * x holds
( len f = len g & ( for i being Element of NAT st 1 <= i & i <= len f holds
g /. i = r * (f /. i) ) )
let f, g be FinSequence of REAL ; :: thesis: for r being Real st f = x & g = r * x holds
( len f = len g & ( for i being Element of NAT st 1 <= i & i <= len f holds
g /. i = r * (f /. i) ) )
let r be Real; :: thesis: ( f = x & g = r * x implies ( len f = len g & ( for i being Element of NAT st 1 <= i & i <= len f holds
g /. i = r * (f /. i) ) ) )
assume A1: ( f = x & g = r * x ) ; :: thesis: ( len f = len g & ( for i being Element of NAT st 1 <= i & i <= len f holds
g /. i = r * (f /. i) ) )
then A2: len f = n by FINSEQ_1:def 18;
A3: len g = n by A1, FINSEQ_1:def 18;
set h1 = (dom (id REAL )) --> r;
reconsider h2 = id REAL as Function ;
A4: g = (multreal * <:((dom (id REAL )) --> r),h2:>) * x by A1, FUNCOP_1:def 5;
A5: ( dom <:((dom (id REAL )) --> r),h2:> = (dom ((dom (id REAL )) --> r)) /\ (dom (id REAL )) & ( for u being set st u in dom <:((dom (id REAL )) --> r),h2:> holds
<:((dom (id REAL )) --> r),h2:> . u = [(((dom (id REAL )) --> r) . u),(h2 . u)] ) ) by FUNCT_3:def 8;
for i being Element of NAT st 1 <= i & i <= len f holds
g /. i = r * (f /. i)

proof

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len f implies g /. i = r * (f /. i) )
assume A6: ( 1 <= i & i <= len f ) ; :: thesis: g /. i = r * (f /. i)
then i in Seg (len f) by FINSEQ_1:3;
then i in dom g by A2, A3, FINSEQ_1:def 3;
then A7: g . i = (multreal * <:((dom (id REAL )) --> r),h2:>) . (x . i) by A4, FUNCT_1:22;
A8: dom h2 = REAL by FUNCT_1:34;
A9: dom <:((dom (id REAL )) --> r),h2:> = (dom ((dom (id REAL )) --> r)) /\ REAL by A5, FUNCT_1:34;
A10: f . i = f /. i by A6, FINSEQ_4:24;
A11: dom ((dom (id REAL )) --> r) = dom (id REAL ) by FUNCOP_1:19
.= REAL by FUNCT_1:34 ;
then A12: <:((dom (id REAL )) --> r),h2:> . (x . i) = [(((dom (id REAL )) --> r) . (x . i)),(h2 . (x . i))] by A9, FUNCT_3:def 8;
A13: ((dom (id REAL )) --> r) . (x . i) = r by A8, FUNCOP_1:13;
h2 . (x . i) = x . i by FUNCT_1:34;
then g . i = multreal . r,(f . i) by A1, A7, A9, A11, A12, A13, FUNCT_1:23;
then g . i = r * (f /. i) by A10, BINOP_2:def 11;
hence g /. i = r * (f /. i) by A2, A3, A6, FINSEQ_4:24; :: thesis: verum

end;

hence ( len f = len g & ( for i being Element of NAT st 1 <= i & i <= len f holds
g /. i = r * (f /. i) ) ) by A1, A2, FINSEQ_1:def 18; :: thesis: verum