let D be non empty set ; :: thesis: for f being FinSequence of D * st f = {} holds
(D -concatenation) "**" f = {}
let f be FinSequence of D * ; :: thesis: ( f = {} implies (D -concatenation) "**" f = {} )
assume A1: f = {} ; :: thesis: (D -concatenation) "**" f = {}
D -concatenation is having_a_unity by MONOID_0:67;
then (D -concatenation) "**" f = the_unity_wrt (D -concatenation) by A1, FINSOP_1:def 1
.= {} by MONOID_0:67 ;
hence (D -concatenation) "**" f = {} ; :: thesis: verum