let r be Real; :: thesis: ((#Z 0) + (#Z 2)) . r = 1 + (r * r)
A1: r #Z 1 = r by PREPOWER:35;
r in REAL by XREAL_0:def 1;
hence ((#Z 0) + (#Z 2)) . r = ((#Z 0) . r) + ((#Z 2) . r) by VALUED_1:1
.= (r #Z 0) + ((#Z 2) . r) by TAYLOR_1:def 1
.= (r #Z 0) + (r #Z 2) by TAYLOR_1:def 1
.= 1 + (r #Z (1 + 1)) by PREPOWER:34
.= 1 + (r * r) by A1, TAYLOR_1:1 ;
:: thesis: verum