let a be Real; :: thesis: for p being Rational st a > 0 holds
(1 / a) #Q p = 1 / (a #Q p)
let p be Rational; :: thesis: ( a > 0 implies (1 / a) #Q p = 1 / (a #Q p) )
assume A1: a > 0 ; :: thesis: (1 / a) #Q p = 1 / (a #Q p)
thus (1 / a) #Q p = (denominator p) -Root (1 / (a #Z (numerator p))) by Th42
.= (denominator p) -Root (a #Z (- (numerator p))) by Th41
.= (denominator p) -Root (a #Z (numerator (- p))) by RAT_1:43
.= a #Q (- p) by RAT_1:43
.= 1 / (a #Q p) by A1, Th54 ; :: thesis: verum