let a, b, r be Real; :: thesis: sin ((a * r) + b) = (sin * (AffineMap (a,b))) . r
A1: r in REAL by XREAL_0:def 1;
thus sin ((a * r) + b) = sin . ((a * r) + b) by SIN_COS:def 17
.= sin . ((AffineMap (a,b)) . r) by FCONT_1:def 4
.= (sin * (AffineMap (a,b))) . r by A1, FUNCT_2:15 ; :: thesis: verum