let a, r, b be real number ; :: thesis: sin ((a * r) + b) = (sin * (AffineMap a,b)) . r
A1: r is Real by XREAL_0:def 1;
thus sin ((a * r) + b) = sin . ((a * r) + b) by SIN_COS:def 21
.= sin . ((AffineMap a,b) . r) by JORDAN16:def 3
.= (sin * (AffineMap a,b)) . r by A1, FUNCT_2:21 ; :: thesis: verum