reconsider e = 1. K, o = 0. K as Element of carr f by XBOOLE_0:def 3;
take doubleLoopStr(# (carr f),(addemb f),(multemb f),e,o #) ; :: thesis: ( the carrier of doubleLoopStr(# (carr f),(addemb f),(multemb f),e,o #) = carr f & the addF of doubleLoopStr(# (carr f),(addemb f),(multemb f),e,o #) = addemb f & the multF of doubleLoopStr(# (carr f),(addemb f),(multemb f),e,o #) = multemb f & the OneF of doubleLoopStr(# (carr f),(addemb f),(multemb f),e,o #) = 1. K & the ZeroF of doubleLoopStr(# (carr f),(addemb f),(multemb f),e,o #) = 0. K )
thus ( the carrier of doubleLoopStr(# (carr f),(addemb f),(multemb f),e,o #) = carr f & the addF of doubleLoopStr(# (carr f),(addemb f),(multemb f),e,o #) = addemb f & the multF of doubleLoopStr(# (carr f),(addemb f),(multemb f),e,o #) = multemb f & the OneF of doubleLoopStr(# (carr f),(addemb f),(multemb f),e,o #) = 1. K & the ZeroF of doubleLoopStr(# (carr f),(addemb f),(multemb f),e,o #) = 0. K ) ; :: thesis: verum