let n be Nat; :: thesis: 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 )
let r be Real; :: thesis: ( r is irrational implies ( (rfs r) . n <> 0 & ((rfs r) . 1) * ((rfs r) . 2) <> 0 & (((scf r) . 1) * ((rfs r) . 2)) + 1 <> 0 ) )
assume A1: r is irrational ; :: thesis: ( (rfs r) . n <> 0 & ((rfs r) . 1) * ((rfs r) . 2) <> 0 & (((scf r) . 1) * ((rfs r) . 2)) + 1 <> 0 )
A2: (rfs r) . n <> 0
proof
assume (rfs r) . n = 0 ; :: thesis: contradiction
then consider n1 being Nat such that
A4: (rfs r) . n1 = 0 ;
for m being Nat st n1 <= m holds
(scf r) . m = 0 by A4, REAL_3:28;
hence contradiction by A1, REAL_3:42; :: thesis: verum
end;
A5: ( (rfs r) . 1 <> 0 & (rfs r) . 2 <> 0 ) by A1, Th2;
(rfs r) . 1 = ((scf r) . 1) + (1 / ((rfs r) . (1 + 1))) by Th1;
then ((rfs r) . 1) * ((rfs r) . 2) = (((scf r) . 1) * ((rfs r) . 2)) + ((1 / ((rfs r) . 2)) * ((rfs r) . 2))
.= (((scf r) . 1) * ((rfs r) . 2)) + 1 by XCMPLX_1:106, A5 ;
hence ( (rfs r) . n <> 0 & ((rfs r) . 1) * ((rfs r) . 2) <> 0 & (((scf r) . 1) * ((rfs r) . 2)) + 1 <> 0 ) by A2, A5; :: thesis: verum