let n be 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, CARD_1:def 7;
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 7;
A5: len g = n by A2, CARD_1:def 7;
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:13
.= REAL by FUNCT_1:17 ;
reconsider xi = x . i as Element of REAL by XREAL_0:def 1;
dom h2 = REAL by FUNCT_1:17;
then A8: ((dom (id REAL)) --> r) . xi = r by FUNCOP_1:7;
assume A9: ( 1 <= i & i <= len f ) ; :: thesis: g /. i = r * (f /. i)
then A10: f . i = f /. i by FINSEQ_4:15;
i in Seg (len f) by A9, FINSEQ_1:1;
then i in dom g by A3, A5, FINSEQ_1:def 3;
then A11: g . i = (multreal * <:((dom (id REAL)) --> r),h2:>) . (x . i) by A6, FUNCT_1:12;
A12: dom <:((dom (id REAL)) --> r),h2:> = (dom ((dom (id REAL)) --> r)) /\ REAL by A4, FUNCT_1:17;
then <:((dom (id REAL)) --> r),h2:> . (x . i) = [(((dom (id REAL)) --> r) . xi),(h2 . xi)] by A7, FUNCT_3:def 7;
then g . i = multreal . (r,(f . i)) by A1, A11, A12, A7, A8, FUNCT_1:13;
then g . i = r * (f /. i) by A10, BINOP_2:def 11;
hence g /. i = r * (f /. i) by A3, A5, A9, FINSEQ_4:15; :: 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, CARD_1:def 7; :: thesis: verum