reconsider i = id the carrier of UA as Element of UAEnd UA by Th2;
take multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) ; :: thesis: ( the carrier of multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = UAEnd UA & the multF of multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = UAEndComp UA & 1. multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = id the carrier of UA )
thus ( the carrier of multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = UAEnd UA & the multF of multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = UAEndComp UA & 1. multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = id the carrier of UA ) ; :: thesis: verum