let n be natural number ; :: thesis: for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL ,REAL st Z c= dom (f1 / f2) holds
for x being Real st x in Z holds
((f1 / f2) . x) #Z n = ((f1 . x) #Z n) / ((f2 . x) #Z n)
let Z be open Subset of REAL ; :: thesis: for f1, f2 being PartFunc of REAL ,REAL st Z c= dom (f1 / f2) holds
for x being Real st x in Z holds
((f1 / f2) . x) #Z n = ((f1 . x) #Z n) / ((f2 . x) #Z n)
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: ( Z c= dom (f1 / f2) implies for x being Real st x in Z holds
((f1 / f2) . x) #Z n = ((f1 . x) #Z n) / ((f2 . x) #Z n) )
assume A1: Z c= dom (f1 / f2) ; :: thesis: for x being Real st x in Z holds
((f1 / f2) . x) #Z n = ((f1 . x) #Z n) / ((f2 . x) #Z n)
let x be Real; :: thesis: ( x in Z implies ((f1 / f2) . x) #Z n = ((f1 . x) #Z n) / ((f2 . x) #Z n) )
assume x in Z ; :: thesis: ((f1 / f2) . x) #Z n = ((f1 . x) #Z n) / ((f2 . x) #Z n)
then ((f1 / f2) . x) #Z n = ((f1 . x) / (f2 . x)) #Z n by A1, RFUNCT_1:def 4
.= ((f1 . x) / (f2 . x)) |^ n by PREPOWER:46
.= ((f1 . x) |^ n) / ((f2 . x) |^ n) by PREPOWER:15
.= ((f1 . x) #Z n) / ((f2 . x) |^ n) by PREPOWER:46
.= ((f1 . x) #Z n) / ((f2 . x) #Z n) by PREPOWER:46 ;
hence ((f1 / f2) . x) #Z n = ((f1 . x) #Z n) / ((f2 . x) #Z n) ; :: thesis: verum