let a, b, c be Ordinal; :: thesis: ( c in b implies b -leading_coeff (c *^ (exp (b,a))) = c )
assume A1: c in b ; :: thesis: b -leading_coeff (c *^ (exp (b,a))) = c
per cases ( 0 in c or not 0 in c ) ;
suppose A2: 0 in c ; :: thesis: b -leading_coeff (c *^ (exp (b,a))) = c
A3: 0 in exp (b,a) by A1, ORDINAL1:14;
thus b -leading_coeff (c *^ (exp (b,a))) = (c *^ (exp (b,a))) div^ (exp (b,a)) by A1, A2, ORDINAL5:58
.= ((c *^ (exp (b,a))) +^ 0) div^ (exp (b,a)) by ORDINAL2:27
.= c by A3, ORDINAL3:66 ; :: thesis: verum
end;
suppose not 0 in c ; :: thesis: b -leading_coeff (c *^ (exp (b,a))) = c
then A4: c = 0 by ORDINAL1:14;
hence b -leading_coeff (c *^ (exp (b,a))) = b -leading_coeff 0 by ORDINAL2:35
.= c by A4, ORDINAL3:70 ;
:: thesis: verum
end;
end;