Theorem T000742