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 :: thesis: for F being FinSequence of D *
for p being Element of D * st S₁[F] holds
S₁[F ^ <*p*>]

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 Th3
.= (Sum (Card F)) + (len (FlattenSeq <*p*>)) by A2, FINSEQ_1:22
.= (Sum (Card F)) + (len p) by Th1
.= Sum ((Card F) ^ <*(len p)*>) by RVSUM_1:74
.= Sum ((Card F) ^ (Card <*p*>)) by Th23
.= Sum (Card (F ^ <*p*>)) by Th24 ;
hence S₁[F ^ <*p*>] ; :: thesis: verum

end;

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