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