reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th7;
take H = multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #); :: thesis: ( the carrier of H = MSAEnd U1 & the multF of H = MSAEndComp U1 & 1. H = id the Sorts of U1 )
thus the carrier of H = MSAEnd U1 ; :: thesis: ( the multF of H = MSAEndComp U1 & 1. H = id the Sorts of U1 )
thus the multF of H = MSAEndComp U1 ; :: thesis: 1. H = id the Sorts of U1
thus 1. H = id the Sorts of U1 ; :: thesis: verum