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:35
.= (id REAL) . x ;
hence (#Z 1) . x = (id REAL) . x ; :: thesis: verum

end;

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