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:25;
s * |[r]| = s * rr by EUCLID:69
.= <*(s * r)*> by RVSUM_1:69 ;
hence s * |[r]| = |[(s * r)]| by EUCLID:69; :: thesis: verum