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