let a, b, c 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:35;
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:31;
then A4: denominator ((a *^ c) / (b *^ c)) = RED ((b *^ c),(a *^ c)) by Th42
.= RED (b,a) by A1, Th28
.= denominator (a / b) by A2, Th42 ;
numerator ((a *^ c) / (b *^ c)) = RED ((a *^ c),(b *^ c)) by A3, Th42
.= RED (a,b) by A1, Th28
.= numerator (a / b) by A2, Th42 ;
hence (a *^ c) / (b *^ c) = (numerator (a / b)) / (denominator (a / b)) by A4, Th39
.= a / b by Th39 ;
:: thesis: verum
end;
end;