take Q ; :: thesis: ( the carrier of Q c= the carrier of Q & the multF of Q = the multF of Q || the carrier of Q & the OneF of Q = the OneF of Q )
thus ( the carrier of Q c= the carrier of Q & the multF of Q = the multF of Q || the carrier of Q & the OneF of Q = the OneF of Q ) ; :: thesis: verum