let a, b, r be Real; :: thesis: r (#) (AffineMap (a,b)) = AffineMap ((r * a),(r * b))
D1: dom (r (#) (AffineMap (a,b))) = REAL by FUNCT_2:def 1;
D2: REAL = dom (AffineMap ((r * a),(r * b))) by FUNCT_2:def 1;
for x being object st x in dom (AffineMap ((r * a),(r * b))) holds
(r (#) (AffineMap (a,b))) . x = (AffineMap ((r * a),(r * b))) . x

proof

let x be object ; :: thesis: ( x in dom (AffineMap ((r * a),(r * b))) implies (r (#) (AffineMap (a,b))) . x = (AffineMap ((r * a),(r * b))) . x )
assume x in dom (AffineMap ((r * a),(r * b))) ; :: thesis: (r (#) (AffineMap (a,b))) . x = (AffineMap ((r * a),(r * b))) . x
then reconsider x = x as Real ;
(r (#) (AffineMap (a,b))) . x = r * ((AffineMap (a,b)) . x) by VALUED_1:6
.= r * ((a * x) + b) by FCONT_1:def 4
.= ((r * a) * x) + (r * b)
.= (AffineMap ((r * a),(r * b))) . x by FCONT_1:def 4 ;
hence (r (#) (AffineMap (a,b))) . x = (AffineMap ((r * a),(r * b))) . x ; :: thesis: verum

end;

hence r (#) (AffineMap (a,b)) = AffineMap ((r * a),(r * b)) by FUNCT_1:2, D1, D2; :: thesis: verum