let n be Nat; :: thesis: for r being Real holds
( dom ((#Z n) / ((#Z 0) + (#Z 2))) = REAL & (#Z n) / ((#Z 0) + (#Z 2)) is continuous & ((#Z n) / ((#Z 0) + (#Z 2))) . r = (r |^ n) / (1 + (r ^2)) )
let r be Real; :: thesis: ( dom ((#Z n) / ((#Z 0) + (#Z 2))) = REAL & (#Z n) / ((#Z 0) + (#Z 2)) is continuous & ((#Z n) / ((#Z 0) + (#Z 2))) . r = (r |^ n) / (1 + (r ^2)) )
set Z0 = #Z 0;
set Z2 = #Z 2;
set Zn = #Z n;
set f = (#Z n) / ((#Z 0) + (#Z 2));
A1: ( dom (#Z n) = REAL & REAL = dom ((#Z 0) + (#Z 2)) ) by FUNCT_2:def 1;
hence A2: dom ((#Z n) / ((#Z 0) + (#Z 2))) = REAL /\ (REAL \ {}) by Lm6, RFUNCT_1:def 1
.= REAL ;
:: thesis: ( (#Z n) / ((#Z 0) + (#Z 2)) is continuous & ((#Z n) / ((#Z 0) + (#Z 2))) . r = (r |^ n) / (1 + (r ^2)) )
A3: ( (#Z n) | REAL is continuous & ((#Z 0) + (#Z 2)) | REAL is continuous ) ;
REAL c= (dom (#Z n)) /\ (dom ((#Z 0) + (#Z 2))) by A1;
then ((#Z n) / ((#Z 0) + (#Z 2))) | REAL is continuous by Lm6, A3, FCONT_1:24;
hence (#Z n) / ((#Z 0) + (#Z 2)) is continuous ; :: thesis: ((#Z n) / ((#Z 0) + (#Z 2))) . r = (r |^ n) / (1 + (r ^2))
(#Z n) . r = r #Z n by TAYLOR_1:def 1
.= r |^ n by PREPOWER:36 ;
hence ((#Z n) / ((#Z 0) + (#Z 2))) . r = (r |^ n) * ((((#Z 0) + (#Z 2)) . r) ") by XREAL_0:def 1, A2, RFUNCT_1:def 1
.= (r |^ n) / (1 + (r ^2)) by Lm5 ;
:: thesis: verum