let n be Nat; :: 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 1
.= ((f1 . x) / (f2 . x)) |^ n by PREPOWER:36
.= ((f1 . x) |^ n) / ((f2 . x) |^ n) by PREPOWER:8
.= ((f1 . x) #Z n) / ((f2 . x) |^ n) by PREPOWER:36
.= ((f1 . x) #Z n) / ((f2 . x) #Z n) by PREPOWER:36 ;
hence ((f1 / f2) . x) #Z n = ((f1 . x) #Z n) / ((f2 . x) #Z n) ; :: thesis: verum