set p = the FinSequence;
set o = the BinOp of { the FinSequence};
set e = the Element of { the FinSequence};
take G = multLoopStr(# { the FinSequence}, the BinOp of { the FinSequence}, the Element of { the FinSequence} #); :: 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 = the Element of { the FinSequence} as Element of G ;
reconsider o = the BinOp of { the FinSequence} as BinOp of G ;

now :: thesis: for b being Element of G holds
( o . (e,b) = b & o . (b,e) = b )

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

end;

hence H₃(G) is_a_unity_wrt H₂(G) by BINOP_1:3; :: 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