take K ; :: thesis: ( the carrier of K c= the carrier of K & the addF of K = the addF of K || the carrier of K & the multF of K = the multF of K || the carrier of K & 1. K = 1. K & 0. K = 0. K )
thus ( the carrier of K c= the carrier of K & the addF of K = the addF of K || the carrier of K & the multF of K = the multF of K || the carrier of K & 1. K = 1. K & 0. K = 0. K ) by RELSET_1:19; :: thesis: verum