let D, E be set ; :: thesis: for F being FinSequence of D *
for G being FinSequence of E * st Card F = Card G holds
len (FlattenSeq F) = len (FlattenSeq G)
let F be FinSequence of D * ; :: thesis: for G being FinSequence of E * st Card F = Card G holds
len (FlattenSeq F) = len (FlattenSeq G)
let G be FinSequence of E * ; :: thesis: ( Card F = Card G implies len (FlattenSeq F) = len (FlattenSeq G) )
assume Card F = Card G ; :: thesis: len (FlattenSeq F) = len (FlattenSeq G)
hence len (FlattenSeq F) = Sum (Card G) by Th26
.= len (FlattenSeq G) by Th26 ;
:: thesis: verum