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

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

hence
#R 1 = (AffineMap (1,0)) | (right_open_halfline 0)
by BA, FUNCT_1:2; :: thesis: verum
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;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