let r be Rational; :: thesis: for a being Element of F_Rat st a = r holds
a |^ 3 = r |^ 3
let a be Element of F_Rat; :: thesis: ( a = r implies a |^ 3 = r |^ 3 )
assume A: a = r ; :: thesis: a |^ 3 = r |^ 3
B: a |^ 3 = a |^ (2 + 1)
.= (a |^ 2) * (a |^ 1) by BINOM:10
.= (a |^ (1 + 1)) * a by BINOM:8
.= ((a |^ 1) * (a |^ 1)) * a by BINOM:10
.= (a * (a |^ 1)) * a by BINOM:8
.= (a * a) * a by BINOM:8 ;
r |^ 3 = r |^ (2 + 1)
.= (r |^ (1 + 1)) * r by NEWTON:6
.= ((r |^ 1) * r) * r by NEWTON:6
.= (r * r) * r ;
hence a |^ 3 = r |^ 3 by A, B; :: thesis: verum