take L ; :: thesis: ( the carrier of L c= the carrier of L & 0. L = 0. L & the addF of L = the addF of L || the carrier of L & the lmult of L = the lmult of L | [: the carrier of INT.Ring, the carrier of L:] & the scalar of L = the scalar of L || the carrier of L )
thus ( the carrier of L c= the carrier of L & 0. L = 0. L & the addF of L = the addF of L || the carrier of L & the lmult of L = the lmult of L | [: the carrier of INT.Ring, the carrier of L:] & the scalar of L = the scalar of L || the carrier of L ) ; :: thesis: verum