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