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

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