for x being Element of REAL holds (#Z 1) . x = (id REAL ) . x

proof

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

end;

hence #Z 1 = id REAL by FUNCT_2:113; :: thesis: verum