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