let b, a, c be ordinal number ; :: thesis: ( b <> 0 implies a mod^ (exp b,c) in exp b,c )
assume A0: b <> 0 ; :: thesis: a mod^ (exp b,c) in exp b,c
set n = a div^ (exp b,c);
exp b,c <> 0 by A0, ORDINAL4:22;
then consider d being ordinal number such that
A2: ( a = ((a div^ (exp b,c)) *^ (exp b,c)) +^ d & d in exp b,c ) by ORDINAL3:def 7;
d = a -^ ((a div^ (exp b,c)) *^ (exp b,c)) by A2, ORDINAL3:65
.= a mod^ (exp b,c) by ORDINAL3:def 8 ;
hence a mod^ (exp b,c) in exp b,c by A2; :: thesis: verum