let A, B, C be Ordinal; :: thesis: ( A in B *^ C implies ( A div^ C in B & A mod^ C in C ) )
assume A1: A in B *^ C ; :: thesis: ( A div^ C in B & A mod^ C in C )
then C <> {} by ORDINAL2:55;
then A2: ex D being Ordinal st
( A = ((A div^ C) *^ C) +^ D & D in C ) by Def7;
assume A3: ( not A div^ C in B or not A mod^ C in C ) ; :: thesis: contradiction
A = ((A div^ C) *^ C) +^ (A mod^ C) by Th78;
then B c= A div^ C by A2, A3, Th24, ORDINAL1:26;
then ( B *^ C c= (A div^ C) *^ C & (A div^ C) *^ C c= A ) by A2, Th27, ORDINAL2:58;
hence contradiction by A1, ORDINAL1:7; :: thesis: verum