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