take
A
; :: thesis: ( the carrier of A c= the carrier of A & 1. A = 1. A & 0. A = 0. A & the addF of A = the addF of A || the carrier of A & the multF of A = the multF of A || the carrier of A & the lmult of A = the lmult of A | [: the carrier of L, the carrier of A:] )

thus ( the carrier of A c= the carrier of A & 1. A = 1. A & 0. A = 0. A & the addF of A = the addF of A || the carrier of A & the multF of A = the multF of A || the carrier of A & the lmult of A = the lmult of A | [: the carrier of L, the carrier of A:] ) ; :: thesis: verum

thus ( the carrier of A c= the carrier of A & 1. A = 1. A & 0. A = 0. A & the addF of A = the addF of A || the carrier of A & the multF of A = the multF of A || the carrier of A & the lmult of A = the lmult of A | [: the carrier of L, the carrier of A:] ) ; :: thesis: verum