now :: thesis: for s1 being CompositionSeries of G ex x being set st
( x c= dom s1 & s1 = s1 * (Sgm x) )

let s1 be CompositionSeries of G; :: thesis: ex x being set st
( x c= dom s1 & s1 = s1 * (Sgm x) )
set x = dom s1;
reconsider x = dom s1 as set ;
take x = x; :: thesis: ( x c= dom s1 & s1 = s1 * (Sgm x) )
thus x c= dom s1 ; :: thesis: s1 = s1 * (Sgm x)
set i = len s1;
Sgm x = Sgm (Seg (len s1)) by FINSEQ_1:def 3
.= idseq (len s1) by FINSEQ_3:48 ;
hence s1 = s1 * (Sgm x) by FINSEQ_2:54; :: thesis: verum

end;

hence for s1 being CompositionSeries of G ex x being set st
( x c= dom s1 & s1 = s1 * (Sgm x) ) ; :: thesis: verum