set f = #R 1;
set g = (AffineMap (1,0)) | (right_open_halfline 0);
A1: dom (#R 1) = right_open_halfline 0 by TAYLOR_1:def 4;
dom (AffineMap (1,0)) = REAL by FUNCT_2:def 1;
then BA: dom (#R 1) = dom ((AffineMap (1,0)) | (right_open_halfline 0)) by A1, RELAT_1:62;
reconsider p = 1 as Real ;
for x being object st x in dom (#R 1) holds
(#R 1) . x = ((AffineMap (1,0)) | (right_open_halfline 0)) . x

proof

let x be object ; :: thesis: ( x in dom (#R 1) implies (#R 1) . x = ((AffineMap (1,0)) | (right_open_halfline 0)) . x )
assume x in dom (#R 1) ; :: thesis: (#R 1) . x = ((AffineMap (1,0)) | (right_open_halfline 0)) . x
then reconsider xx = x as Element of right_open_halfline 0 by TAYLOR_1:def 4;
A2: xx > 0 by XXREAL_1:4;
(#R 1) . x = xx #R p by TAYLOR_1:def 4
.= (1 * xx) + 0 by PREPOWER:72, A2
.= (AffineMap (1,0)) . xx by FCONT_1:def 4
.= ((AffineMap (1,0)) | (right_open_halfline 0)) . x by FUNCT_1:49 ;
hence (#R 1) . x = ((AffineMap (1,0)) | (right_open_halfline 0)) . x ; :: thesis: verum

end;

hence #R 1 = (AffineMap (1,0)) | (right_open_halfline 0) by BA, FUNCT_1:2; :: thesis: verum