set p = the FinSequence;
set o = the BinOp of { the FinSequence};
take G = multMagma(# { the FinSequence}, the BinOp of { the FinSequence} #); :: thesis: ( G is unital & G is commutative & G is associative & G is cancelable & G is idempotent & G is invertible & G is uniquely-decomposable & G is constituted-Functions & G is constituted-FinSeqs & G is strict )
thus ( H₂(G) is having_a_unity & H₂(G) is commutative & H₂(G) is associative & H₂(G) is cancelable & H₂(G) is idempotent & H₂(G) is invertible & H₂(G) is uniquely-decomposable ) by Th3; :: according to MONOID_0:def 10,MONOID_0:def 11,MONOID_0:def 12,MONOID_0:def 13,MONOID_0:def 16,MONOID_0:def 19,MONOID_0:def 20 :: thesis: ( G is constituted-Functions & G is constituted-FinSeqs & G is strict )
thus ( ( for x being Element of G holds x is Function ) & ( for x being Element of G holds x is FinSequence ) ) by TARSKI:def 1; :: according to MONOID_0:def 1,MONOID_0:def 2 :: thesis: G is strict
thus G is strict ; :: thesis: verum