let N be Nat; :: thesis: for r being Real
for seq being Real_Sequence of N holds |.(r * seq).| = |.r.| (#) |.seq.|
let r be Real; :: thesis: for seq being Real_Sequence of N holds |.(r * seq).| = |.r.| (#) |.seq.|
let seq be Real_Sequence of N; :: thesis: |.(r * seq).| = |.r.| (#) |.seq.|
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: |.(r * seq).| . n = (|.r.| (#) |.seq.|) . n
thus |.(r * seq).| . n = |.((r * seq) . n).| by Def6
.= |.(r * (seq . n)).| by Th5
.= |.r.| * |.(seq . n).| by Th7
.= |.r.| * (|.seq.| . n) by Def6
.= (|.r.| (#) |.seq.|) . n by SEQ_1:9 ; :: thesis: verum