let a, b, c be Ordinal; ( b <> 0 implies a mod^ (exp (b,c)) in exp (b,c) )
assume A1:
b <> 0
; a mod^ (exp (b,c)) in exp (b,c)
set n = a div^ (exp (b,c));
exp (b,c) <> 0
by A1;
then consider d being Ordinal such that
A2:
( a = ((a div^ (exp (b,c))) *^ (exp (b,c))) +^ d & d in exp (b,c) )
by ORDINAL3:def 6;
d =
a -^ ((a div^ (exp (b,c))) *^ (exp (b,c)))
by A2, ORDINAL3:52
.=
a mod^ (exp (b,c))
by ORDINAL3:def 7
;
hence
a mod^ (exp (b,c)) in exp (b,c)
by A2; verum