consider p being FinSequence, o being BinOp of {p}, e being Element of {p};
take G = multLoopStr(# {p},o,e #); :: thesis: ( G is well-unital & G is commutative & G is associative & G is cancelable & G is idempotent & G is invertible & G is uniquely-decomposable & G is unital & G is constituted-Functions & G is constituted-FinSeqs & G is strict )
reconsider e = e as Element of G ;
reconsider o = o as BinOp of G ;

now

let b be Element of G; :: thesis: ( o . e,b = b & o . b,e = b )
( o . e,b = p & o . b,e = p & b = p ) by TARSKI:def 1;
hence ( o . e,b = b & o . b,e = b ) ; :: thesis: verum

end;

hence H₃(G) is_a_unity_wrt H₂(G) by BINOP_1:11; :: according to MONOID_0:def 21 :: thesis: ( G is commutative & G is associative & G is cancelable & G is idempotent & G is invertible & G is uniquely-decomposable & G is unital & G is constituted-Functions & G is constituted-FinSeqs & G is strict )
hence ( 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 & ex e being Element of G st e is_a_unity_wrt H₂(G) ) by Th3; :: according to SETWISEO:def 2,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