let c, a, b be natural Ordinal; :: thesis: ( c <> {} implies (a *^ c) / (b *^ c) = a / b )
assume A1: c <> {} ; :: thesis: (a *^ c) / (b *^ c) = a / b

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

suppose b = {} ; :: thesis: (a *^ c) / (b *^ c) = a / b

then ( a / b = {} & b *^ c = {} ) by Def10, ORDINAL2:52;
hence (a *^ c) / (b *^ c) = a / b by Def10; :: thesis: verum

end;

suppose A2: b <> {} ; :: thesis: (a *^ c) / (b *^ c) = a / b

then A3: b *^ c <> {} by A1, ORDINAL3:34;
then A4: numerator ((a *^ c) / (b *^ c)) = RED (a *^ c),(b *^ c) by Th48
.= RED a,b by A1, Th33
.= numerator (a / b) by A2, Th48 ;
denominator ((a *^ c) / (b *^ c)) = RED (b *^ c),(a *^ c) by A3, Th48
.= RED b,a by A1, Th33
.= denominator (a / b) by A2, Th48 ;
hence (a *^ c) / (b *^ c) = (numerator (a / b)) / (denominator (a / b)) by A4, Th45
.= a / b by Th45 ;
:: thesis: verum

end;

end;