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) ) )
reconsider h2 = id REAL as Function ;
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 that
A1: f = x and
A2: 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) ) )
A3: len f = n by A1, FINSEQ_1:def 18;
set h1 = (dom (id REAL )) --> r;
A4: dom <:((dom (id REAL )) --> r),h2:> = (dom ((dom (id REAL )) --> r)) /\ (dom (id REAL )) by FUNCT_3:def 8;
A5: len g = n by A2, FINSEQ_1:def 18;
A6: g = (multreal * <:((dom (id REAL )) --> r),h2:>) * x by A2, FUNCOP_1:def 5;
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) )
A7: dom ((dom (id REAL )) --> r) = dom (id REAL ) by FUNCOP_1:19
.= REAL by FUNCT_1:34 ;
dom h2 = REAL by FUNCT_1:34;
then A8: ((dom (id REAL )) --> r) . (x . i) = r by FUNCOP_1:13;
A9: h2 . (x . i) = x . i by FUNCT_1:34;
assume A10: ( 1 <= i & i <= len f ) ; :: thesis: g /. i = r * (f /. i)
then A11: f . i = f /. i by FINSEQ_4:24;
i in Seg (len f) by A10, FINSEQ_1:3;
then i in dom g by A3, A5, FINSEQ_1:def 3;
then A12: g . i = (multreal * <:((dom (id REAL )) --> r),h2:>) . (x . i) by A6, FUNCT_1:22;
A13: dom <:((dom (id REAL )) --> r),h2:> = (dom ((dom (id REAL )) --> r)) /\ REAL by A4, FUNCT_1:34;
then <:((dom (id REAL )) --> r),h2:> . (x . i) = [(((dom (id REAL )) --> r) . (x . i)),(h2 . (x . i))] by A7, FUNCT_3:def 8;
then g . i = multreal . r,(f . i) by A1, A12, A13, A7, A8, A9, FUNCT_1:23;
then g . i = r * (f /. i) by A11, BINOP_2:def 11;
hence g /. i = r * (f /. i) by A3, A5, A10, 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 A2, A3, FINSEQ_1:def 18; :: thesis: verum