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

proof

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

end;

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