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