let r be Real; :: thesis: for fr being Element of F_Real
for p being FinSequence of REAL
for fp being FinSequence of F_Real st r = fr & p = fp holds
r * p = fr * fp
let fr be Element of F_Real; :: thesis: for p being FinSequence of REAL
for fp being FinSequence of F_Real st r = fr & p = fp holds
r * p = fr * fp
let p be FinSequence of REAL ; :: thesis: for fp being FinSequence of F_Real st r = fr & p = fp holds
r * p = fr * fp
let fp be FinSequence of F_Real; :: thesis: ( r = fr & p = fp implies r * p = fr * fp )
assume that
A1: r = fr and
A2: p = fp ; :: thesis: r * p = fr * fp
A3: len (r * p) = len fp by A2, RVSUM_1:117;
then A4: len (r * p) = len (fr * fp) by Th16;
for i being Nat st 1 <= i & i <= len (r * p) holds
(r * p) . i = (fr * fp) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (r * p) implies (r * p) . i = (fr * fp) . i )
assume ( 1 <= i & i <= len (r * p) ) ; :: thesis: (r * p) . i = (fr * fp) . i
then i in Seg (len fp) by A3, FINSEQ_1:1;
then A5: i in dom (fr * fp) by A3, A4, FINSEQ_1:def 3;
reconsider s = fp . i as Element of F_Real by XREAL_0:def 1;
thus (r * p) . i = fr * s by A1, A2, RVSUM_1:44
.= (fr * fp) . i by A5, FVSUM_1:50 ; :: thesis: verum

end;

hence r * p = fr * fp by A4, FINSEQ_1:14; :: thesis: verum