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 ModuleStr(# H₁(n -Group_over F),H₂(n -Group_over F),H₄(n -Group_over F),d #) ; :: thesis: ( addLoopStr(# the carrier of ModuleStr(# H₁(n -Group_over F),H₂(n -Group_over F),H₄(n -Group_over F),d #), the addF of ModuleStr(# H₁(n -Group_over F),H₂(n -Group_over F),H₄(n -Group_over F),d #), the ZeroF of ModuleStr(# H₁(n -Group_over F),H₂(n -Group_over F),H₄(n -Group_over F),d #) #) = n -Group_over F & the lmult of ModuleStr(# 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 ModuleStr(# H₁(n -Group_over F),H₂(n -Group_over F),H₄(n -Group_over F),d #), the addF of ModuleStr(# H₁(n -Group_over F),H₂(n -Group_over F),H₄(n -Group_over F),d #), the ZeroF of ModuleStr(# H₁(n -Group_over F),H₂(n -Group_over F),H₄(n -Group_over F),d #) #) = n -Group_over F & the lmult of ModuleStr(# H₁(n -Group_over F),H₂(n -Group_over F),H₄(n -Group_over F),d #) = n -Mult_over F ) ; :: thesis: verum