per cases ( m in dom (Rascal n) or not m in dom (Rascal n) ) ;

suppose B1: m in dom (Rascal n) ; :: thesis: (Rascal n) . m is natural

then m in Seg (n + 1) by Def1;
then ( 1 <= m & m <= n + 1 ) by FINSEQ_1:1;
then ( m - 1 >= 1 - 1 & (n + 1) - m >= m - m ) by XREAL_1:9;
then ((m - 1) * ((n + 1) - m)) + 1 is Nat ;
hence (Rascal n) . m is natural by Def1, B1; :: thesis: verum

end;

suppose not m in dom (Rascal n) ; :: thesis: (Rascal n) . m is natural

hence (Rascal n) . m is natural by FUNCT_1:def 2; :: thesis: verum

end;

end;