let a, b, c be Ordinal; ( c in b implies b -leading_coeff (c *^ (exp (b,a))) = c )
assume A1:
c in b
; b -leading_coeff (c *^ (exp (b,a))) = c
per cases
( 0 in c or not 0 in c )
;
suppose A2:
0 in c
;
b -leading_coeff (c *^ (exp (b,a))) = cA3:
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
;
verum end; end;