take doubleLoopStr(# (unionCarrier (S,f,E)),(unionAdd (S,f,E)),(unionMult (S,f,E)),(unionOne (S,f,E)),(unionZero (S,f,E)) #) ; :: thesis: ( the carrier of doubleLoopStr(# (unionCarrier (S,f,E)),(unionAdd (S,f,E)),(unionMult (S,f,E)),(unionOne (S,f,E)),(unionZero (S,f,E)) #) = unionCarrier (S,f,E) & the addF of doubleLoopStr(# (unionCarrier (S,f,E)),(unionAdd (S,f,E)),(unionMult (S,f,E)),(unionOne (S,f,E)),(unionZero (S,f,E)) #) = unionAdd (S,f,E) & the multF of doubleLoopStr(# (unionCarrier (S,f,E)),(unionAdd (S,f,E)),(unionMult (S,f,E)),(unionOne (S,f,E)),(unionZero (S,f,E)) #) = unionMult (S,f,E) & the OneF of doubleLoopStr(# (unionCarrier (S,f,E)),(unionAdd (S,f,E)),(unionMult (S,f,E)),(unionOne (S,f,E)),(unionZero (S,f,E)) #) = unionOne (S,f,E) & the ZeroF of doubleLoopStr(# (unionCarrier (S,f,E)),(unionAdd (S,f,E)),(unionMult (S,f,E)),(unionOne (S,f,E)),(unionZero (S,f,E)) #) = unionZero (S,f,E) )
thus ( the carrier of doubleLoopStr(# (unionCarrier (S,f,E)),(unionAdd (S,f,E)),(unionMult (S,f,E)),(unionOne (S,f,E)),(unionZero (S,f,E)) #) = unionCarrier (S,f,E) & the addF of doubleLoopStr(# (unionCarrier (S,f,E)),(unionAdd (S,f,E)),(unionMult (S,f,E)),(unionOne (S,f,E)),(unionZero (S,f,E)) #) = unionAdd (S,f,E) & the multF of doubleLoopStr(# (unionCarrier (S,f,E)),(unionAdd (S,f,E)),(unionMult (S,f,E)),(unionOne (S,f,E)),(unionZero (S,f,E)) #) = unionMult (S,f,E) & the OneF of doubleLoopStr(# (unionCarrier (S,f,E)),(unionAdd (S,f,E)),(unionMult (S,f,E)),(unionOne (S,f,E)),(unionZero (S,f,E)) #) = unionOne (S,f,E) & the ZeroF of doubleLoopStr(# (unionCarrier (S,f,E)),(unionAdd (S,f,E)),(unionMult (S,f,E)),(unionOne (S,f,E)),(unionZero (S,f,E)) #) = unionZero (S,f,E) ) ; :: thesis: verum