for n being Nat
for r being Real st r is irrational holds
( (rfs r) . n <> 0 & ((rfs r) . 1) * ((rfs r) . 2) <> 0 & (((scf r) . 1) * ((rfs r) . 2)) + 1 <> 0 )