let x be Element of REAL ; :: thesis:
(#Z 1) . x = x #Z 1 by TAYLOR_1:def 1
.= x by PREPOWER:35
.= (id REAL) . x ;
hence (#Z 1) . x = (id REAL) . x ; :: thesis:

end;