thus ( IT is rational-valued implies for n being Element of NAT holds IT . n is Rational ) ; :: thesis: ( ( for n being Element of NAT holds IT . n is Rational ) implies IT is rational-valued )
assume A1: for n being Element of NAT holds IT . n is Rational ; :: thesis: IT is rational-valued

now

let x be set ; :: thesis: IT . b₁ is rational

per cases ( x in dom IT or not x in dom IT ) ;

suppose x in dom IT ; :: thesis: IT . b₁ is rational

then x in NAT by FUNCT_2:def 1;
hence IT . x is rational by A1; :: thesis: verum

end;

suppose not x in dom IT ; :: thesis: IT . b₁ is rational

hence IT . x is rational by FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

hence IT is rational-valued by VALUED_0:10; :: thesis: verum