n -Group_over F = addLoopStr(# (n -tuples_on the carrier of F),(product the addF of F,n),(n |-> (0. F)) #) by Def3;
then reconsider d = n -Mult_over F as Function of [:the carrier of F,the carrier of (n -Group_over F):],the carrier of (n -Group_over F) ;
set G = n -Group_over F;
take VectSpStr(# H₁(n -Group_over F),H₂(n -Group_over F),H₄(n -Group_over F),d #) ; :: thesis: ( addLoopStr(# the carrier of VectSpStr(# H₁(n -Group_over F),H₂(n -Group_over F),H₄(n -Group_over F),d #),the addF of VectSpStr(# H₁(n -Group_over F),H₂(n -Group_over F),H₄(n -Group_over F),d #),the ZeroF of VectSpStr(# H₁(n -Group_over F),H₂(n -Group_over F),H₄(n -Group_over F),d #) #) = n -Group_over F & the lmult of VectSpStr(# H₁(n -Group_over F),H₂(n -Group_over F),H₄(n -Group_over F),d #) = n -Mult_over F )
thus ( addLoopStr(# the carrier of VectSpStr(# H₁(n -Group_over F),H₂(n -Group_over F),H₄(n -Group_over F),d #),the addF of VectSpStr(# H₁(n -Group_over F),H₂(n -Group_over F),H₄(n -Group_over F),d #),the ZeroF of VectSpStr(# H₁(n -Group_over F),H₂(n -Group_over F),H₄(n -Group_over F),d #) #) = n -Group_over F & the lmult of VectSpStr(# H₁(n -Group_over F),H₂(n -Group_over F),H₄(n -Group_over F),d #) = n -Mult_over F ) ; :: thesis: verum