let r be real number ; :: thesis: for s being Real holds s * |[r]| = |[(s * r)]|
let s be Real; :: thesis: s * |[r]| = |[(s * r)]|
reconsider r = r as Real by XREAL_0:def 1;
reconsider rr = |[r]| as Element of REAL 1 by EUCLID:22;
s * |[r]| = s * rr by EUCLID:65
.= <*(s * r)*> by RVSUM_1:47 ;
hence s * |[r]| = |[(s * r)]| ; :: thesis: verum