let a, b be Ordinal; :: thesis: ( 1 in b implies b -leading_coeff (exp (b,a)) = 1 )
assume A1: 1 in b ; :: thesis: b -leading_coeff (exp (b,a)) = 1
thus b -leading_coeff (exp (b,a)) = b -leading_coeff (1 *^ (exp (b,a))) by ORDINAL2:39
.= 1 by A1, Th57 ; :: thesis: verum