theorem Th3: :: FDIFF_8:3

for n being Nat
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)