let D be set ; :: thesis: for F being FinSequence of D * holds len (FlattenSeq F) = Sum (Card F)
defpred S₁[ FinSequence of D * ] means len (FlattenSeq $1) = Sum (Card $1);

A1: now

let F be FinSequence of D * ; :: thesis: for p being Element of D * st S₁[F] holds
S₁[F ^ <*p*>]
let p be Element of D * ; :: thesis: ( S₁[F] implies S₁[F ^ <*p*>] )
assume A2: S₁[F] ; :: thesis: S₁[F ^ <*p*>]
len (FlattenSeq (F ^ <*p*>)) = len ((FlattenSeq F) ^ (FlattenSeq <*p*>)) by Th21D
.= (Sum (Card F)) + (len (FlattenSeq <*p*>)) by A2, FINSEQ_1:35
.= (Sum (Card F)) + (len p) by Th13D
.= Sum ((Card F) ^ <*(len p)*>) by RVSUM_1:104
.= Sum ((Card F) ^ (Card <*p*>)) by Th12
.= Sum (Card (F ^ <*p*>)) by Th13 ;
hence S₁[F ^ <*p*>] ; :: thesis: verum

end;

A3: S₁[ <*> (D * )] by RVSUM_1:102;
thus for F being FinSequence of D * holds S₁[F] from FINSEQ_2:sch 2(A3, A1); :: thesis: verum