let a, b be Real; :: thesis: AffineMap (a,b) = (a (#) (#Z 1)) + (b (#) (#Z 0))
for x being object st x in REAL holds
(AffineMap (a,b)) . x = ((a (#) (#Z 1)) + (b (#) (#Z 0))) . x

proof

let x be object ; :: thesis: ( x in REAL implies (AffineMap (a,b)) . x = ((a (#) (#Z 1)) + (b (#) (#Z 0))) . x )
assume x in REAL ; :: thesis: (AffineMap (a,b)) . x = ((a (#) (#Z 1)) + (b (#) (#Z 0))) . x
then reconsider x = x as Element of REAL ;
((a (#) (#Z 1)) + (b (#) (#Z 0))) . x = ((a (#) (#Z 1)) . x) + ((b (#) (#Z 0)) . x) by VALUED_1:1
.= (a * ((#Z 1) . x)) + ((b (#) (#Z 0)) . x) by VALUED_1:6
.= (a * ((#Z 1) . x)) + (b * ((#Z 0) . x)) by VALUED_1:6
.= (a * (x #Z 1)) + (b * ((#Z 0) . x)) by TAYLOR_1:def 1
.= (a * (x #Z 1)) + (b * (x #Z 0)) by TAYLOR_1:def 1
.= (a * (x |^ 1)) + (b * (x #Z 0)) by PREPOWER:36
.= (a * x) + (b * 1) by PREPOWER:34
.= (AffineMap (a,b)) . x by FCONT_1:def 4 ;
hence (AffineMap (a,b)) . x = ((a (#) (#Z 1)) + (b (#) (#Z 0))) . x ; :: thesis: verum

end;

hence AffineMap (a,b) = (a (#) (#Z 1)) + (b (#) (#Z 0)) by FUNCT_2:12; :: thesis: verum