let A, B be Ordinal; :: thesis: (A div^ B) *^ B c= A

now :: thesis: (A div^ B) *^ B c= A

per cases ( B <> {} or B = {} ) ;

suppose B <> {} ; :: thesis: (A div^ B) *^ B c= A

then ex C being Ordinal st
( A = ((A div^ B) *^ B) +^ C & C in B ) by Def6;
hence (A div^ B) *^ B c= A by Th24; :: thesis: verum

end;

suppose B = {} ; :: thesis: (A div^ B) *^ B c= A

then A div^ B = {} by Def6;
then (A div^ B) *^ B = {} by ORDINAL2:35;
hence (A div^ B) *^ B c= A ; :: thesis: verum

end;

end;

end;

hence (A div^ B) *^ B c= A ; :: thesis: verum