let a be Real; :: thesis: for p being Rational st p = 0 holds

a #Q p = 1

let p be Rational; :: thesis: ( p = 0 implies a #Q p = 1 )

reconsider i = 0 as Integer ;

assume A1: p = 0 ; :: thesis: a #Q p = 1

numerator p = 0 by A1, RAT_1:14;

hence a #Q p = 1 -Root (a #Z i) by A1, RAT_1:19

.= 1 -Root 1 by Th34

.= 1 by Th21 ;

:: thesis: verum

a #Q p = 1

let p be Rational; :: thesis: ( p = 0 implies a #Q p = 1 )

reconsider i = 0 as Integer ;

assume A1: p = 0 ; :: thesis: a #Q p = 1

numerator p = 0 by A1, RAT_1:14;

hence a #Q p = 1 -Root (a #Z i) by A1, RAT_1:19

.= 1 -Root 1 by Th34

.= 1 by Th21 ;

:: thesis: verum