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

a #Q p = a

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

assume that

A1: a > 0 and

A2: p = 1 ; :: thesis: a #Q p = a

A3: denominator p = 1 by A2, RAT_1:17;

numerator p = p by A2, RAT_1:17;

hence a #Q p = 1 -Root a by A2, A3, Th35

.= a by A1, Th21 ;

:: thesis: verum

a #Q p = a

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

assume that

A1: a > 0 and

A2: p = 1 ; :: thesis: a #Q p = a

A3: denominator p = 1 by A2, RAT_1:17;

numerator p = p by A2, RAT_1:17;

hence a #Q p = 1 -Root a by A2, A3, Th35

.= a by A1, Th21 ;

:: thesis: verum