let D be set ; :: thesis: for F being FinSequence of D * holds len (FlattenSeq F) = Sum (Card F)
defpred S1[ 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 S1[F] holds
S1[F ^ <*p*>]
let F be FinSequence of D * ; :: thesis: for p being Element of D * st S1[F] holds
S1[F ^ <*p*>]
let p be Element of D * ; :: thesis: ( S1[F] implies S1[F ^ <*p*>] )
assume A2: S1[F] ; :: thesis: S1[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 S1[F ^ <*p*>] ; :: thesis: verum
end;
A3: S1[ <*> (D *)] by RVSUM_1:72;
thus for F being FinSequence of D * holds S1[F] from FINSEQ_2:sch 2(A3, A1); :: thesis: verum