take
RLSStruct(# (CosetSet (M,k)),(zeroCoset (M,k)),(addCoset (M,k)),(lmultCoset (M,k)) #)
; ( the carrier of RLSStruct(# (CosetSet (M,k)),(zeroCoset (M,k)),(addCoset (M,k)),(lmultCoset (M,k)) #) = CosetSet (M,k) & the addF of RLSStruct(# (CosetSet (M,k)),(zeroCoset (M,k)),(addCoset (M,k)),(lmultCoset (M,k)) #) = addCoset (M,k) & 0. RLSStruct(# (CosetSet (M,k)),(zeroCoset (M,k)),(addCoset (M,k)),(lmultCoset (M,k)) #) = zeroCoset (M,k) & the Mult of RLSStruct(# (CosetSet (M,k)),(zeroCoset (M,k)),(addCoset (M,k)),(lmultCoset (M,k)) #) = lmultCoset (M,k) )
thus
( the carrier of RLSStruct(# (CosetSet (M,k)),(zeroCoset (M,k)),(addCoset (M,k)),(lmultCoset (M,k)) #) = CosetSet (M,k) & the addF of RLSStruct(# (CosetSet (M,k)),(zeroCoset (M,k)),(addCoset (M,k)),(lmultCoset (M,k)) #) = addCoset (M,k) & 0. RLSStruct(# (CosetSet (M,k)),(zeroCoset (M,k)),(addCoset (M,k)),(lmultCoset (M,k)) #) = zeroCoset (M,k) & the Mult of RLSStruct(# (CosetSet (M,k)),(zeroCoset (M,k)),(addCoset (M,k)),(lmultCoset (M,k)) #) = lmultCoset (M,k) )
; verum