let th be real number ; :: thesis: exp_R . th > 0

now

per cases ( th = 0 or th <> 0 ) ;

suppose th = 0 ; :: thesis: exp_R . th > 0

hence exp_R . th > 0 by Lm11; :: thesis: verum

end;

suppose A1: th <> 0 ; :: thesis: exp_R . th > 0

now

per cases ( th < 0 or th > 0 ) by A1;

suppose th < 0 ; :: thesis: exp_R . th > 0

hence exp_R . th > 0 by Th58; :: thesis: verum

end;

suppose th > 0 ; :: thesis: exp_R . th > 0

hence exp_R . th > 0 by Th57; :: thesis: verum

end;

end;

end;

hence exp_R . th > 0 ; :: thesis: verum

end;

end;

end;

hence exp_R . th > 0 ; :: thesis: verum