take RLSStruct(# (CosetSet M,k),(zeroCoset M,k),(addCoset M,k),(lmultCoset M,k) #) ; :: thesis: ( 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 ) ; :: thesis: verum