take G ; :: thesis: ( the carrier of G c= the carrier of G & the addF of G = the addF of G || the carrier of G & 0. G = 0. G )
thus ( the carrier of G c= the carrier of G & the addF of G = the addF of G || the carrier of G & 0. G = 0. G ) ; :: thesis: verum