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

now

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 Def7;
hence (A div^ B) *^ B c= A by Th27; :: thesis: verum

end;

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

then A div^ B = {} by Def7;
then (A div^ B) *^ B = {} by ORDINAL2:52;
hence (A div^ B) *^ B c= A by XBOOLE_1:2; :: thesis: verum

end;

end;

end;

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