now :: thesis: for s1 being CompositionSeries of G ex x being set st

( x c= dom s1 & s1 = s1 * (Sgm x) )

hence
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;( 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

( x c= dom s1 & s1 = s1 * (Sgm x) ) ; :: thesis: verum