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