let n be Nat; :: thesis: for r being Real st r is irrational holds
(rfs r) . n is irrational
let r be Real; :: thesis: ( r is irrational implies (rfs r) . n is irrational )
assume A1: r is irrational ; :: thesis: (rfs r) . n is irrational
set rn = (rfs r) . n;
A3: (scf ((rfs r) . n)) . 0 = [\((rfs ((rfs r) . n)) . 0)/] by REAL_3:def 4
.= [\((rfs r) . n)/] by REAL_3:def 3
.= (scf r) . n by REAL_3:def 4 ;
A4: for m being Nat holds
( (scf ((rfs r) . n)) . m = (scf r) . (n + m) & (rfs ((rfs r) . n)) . m = (rfs r) . (n + m) )

proof

let m be Nat; :: thesis: ( (scf ((rfs r) . n)) . m = (scf r) . (n + m) & (rfs ((rfs r) . n)) . m = (rfs r) . (n + m) )
defpred S₁[ Nat] means ( (scf ((rfs r) . n)) . $1 = (scf r) . (n + $1) & (rfs ((rfs r) . n)) . $1 = (rfs r) . (n + $1) );
A5: S₁[ 0 ] by REAL_3:def 3, A3;
A6: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A7: S₁[m] ; :: thesis: S₁[m + 1]
A9: (rfs ((rfs r) . n)) . (m + 1) = 1 / (frac ((rfs ((rfs r) . n)) . m)) by REAL_3:def 3
.= (rfs r) . ((n + m) + 1) by A7, REAL_3:def 3 ;
(scf ((rfs r) . n)) . (m + 1) = [\((rfs ((rfs r) . n)) . (m + 1))/] by REAL_3:def 4
.= (scf r) . ((n + m) + 1) by A9, REAL_3:def 4 ;
hence S₁[m + 1] by A9; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A5, A6);
hence ( (scf ((rfs r) . n)) . m = (scf r) . (n + m) & (rfs ((rfs r) . n)) . m = (rfs r) . (n + m) ) ; :: thesis: verum

end;

assume A10: (rfs r) . n is rational ; :: thesis: contradiction
consider n1 being Nat such that
A12: for m1 being Nat st m1 >= n1 holds
(scf ((rfs r) . n)) . m1 = 0 by A10, REAL_3:42;
A13: for m1 being Nat st m1 >= n1 holds
(scf r) . (n + m1) = 0

proof

let m1 be Nat; :: thesis: ( m1 >= n1 implies (scf r) . (n + m1) = 0 )
assume A14: m1 >= n1 ; :: thesis: (scf r) . (n + m1) = 0
(scf r) . (n + m1) = (scf ((rfs r) . n)) . m1 by A4
.= 0 by A12, A14 ;
hence (scf r) . (n + m1) = 0 ; :: thesis: verum

end;

for m being Nat st m >= n1 + n holds
(scf r) . m = 0

proof

let m be Nat; :: thesis: ( m >= n1 + n implies (scf r) . m = 0 )
assume A15: m >= n1 + n ; :: thesis: (scf r) . m = 0
A16: m - n >= (n1 + n) - n by A15, XREAL_1:9;
m - n in NAT by A16, INT_1:3;
then reconsider l = m - n as Nat ;
(scf r) . (n + l) = 0 by A13, A16;
hence (scf r) . m = 0 ; :: thesis: verum

end;

hence contradiction by A1, REAL_3:42; :: thesis: verum