let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for F being FinSequence of the carrier of L * holds Sum (FlattenSeq F) = Sum (Sum F)
defpred S₁[ FinSequence of the carrier of L * ] means Sum (FlattenSeq $1) = Sum (Sum $1);
A1: for f being FinSequence of the carrier of L *
for p being Element of the carrier of L * st S₁[f] holds
S₁[f ^ <*p*>]

proof

let f be FinSequence of the carrier of L * ; :: thesis: for p being Element of the carrier of L * st S₁[f] holds
S₁[f ^ <*p*>]
let p be Element of the carrier of L * ; :: thesis: ( S₁[f] implies S₁[f ^ <*p*>] )
assume A2: Sum (FlattenSeq f) = Sum (Sum f) ; :: thesis: S₁[f ^ <*p*>]
thus Sum (FlattenSeq (f ^ <*p*>)) = Sum ((FlattenSeq f) ^ (FlattenSeq <*p*>)) by PRE_POLY:3
.= Sum ((FlattenSeq f) ^ p) by PRE_POLY:1
.= (Sum (Sum f)) + (Sum p) by A2, RLVECT_1:41
.= (Sum (Sum f)) + (Sum <*(Sum p)*>) by RLVECT_1:44
.= Sum ((Sum f) ^ <*(Sum p)*>) by RLVECT_1:41
.= Sum ((Sum f) ^ (Sum <*p*>)) by Th4
.= Sum (Sum (f ^ <*p*>)) by Th5 ; :: thesis: verum

end;

Sum (FlattenSeq (<*> ( the carrier of L *))) = Sum (<*> the carrier of L) ;
then A3: S₁[ <*> ( the carrier of L *)] by Th3;
thus for f being FinSequence of the carrier of L * holds S₁[f] from FINSEQ_2:sch 2(A3, A1); :: thesis: verum