let x be Element of (RAlgebra REAL); :: thesis: x |^ 0 = REAL --> 1
thus x |^ 0 = 1_ (RAlgebra REAL) by BINOM:8
.= REAL --> 1 ; :: thesis: verum