let D be set ; :: thesis: for f being FinSequence of D *
for i being Nat holds Card (f | i) = (Card f) | i

let f be FinSequence of D * ; :: thesis: for i being Nat holds Card (f | i) = (Card f) | i
let i be Nat; :: thesis: Card (f | i) = (Card f) | i
A1: f | i = f | (Seg i) by FINSEQ_1:def 15;
reconsider k = min (i,(len f)) as Nat by TARSKI:1;
dom (Card (f | i)) = dom (f | i) by CARD_3:def 2;
then A2: len (Card (f | i)) = len (f | i) by FINSEQ_3:29
.= min (i,(len f)) by ;
then A3: dom (Card (f | i)) = Seg k by FINSEQ_1:def 3;
A4: dom (Card f) = dom f by CARD_3:def 2;
A5: (Card f) | i = (Card f) | (Seg i) by FINSEQ_1:def 15;
A6: now :: thesis: for j being Nat st j in dom (Card (f | i)) holds
(Card (f | i)) . j = ((Card f) | i) . j
A7: len f = len (Card f) by ;
let j be Nat; :: thesis: ( j in dom (Card (f | i)) implies (Card (f | i)) . b1 = ((Card f) | i) . b1 )
assume A8: j in dom (Card (f | i)) ; :: thesis: (Card (f | i)) . b1 = ((Card f) | i) . b1
per cases ( i <= len f or i > len f ) ;
suppose A9: i <= len f ; :: thesis: (Card (f | i)) . b1 = ((Card f) | i) . b1
A10: 1 <= j by ;
A11: k = i by ;
then j <= i by ;
then j <= len f by ;
then A12: j in dom f by ;
len ((Card f) | i) = i by ;
then A13: dom ((Card f) | i) = Seg i by FINSEQ_1:def 3;
reconsider Cf = Card f as FinSequence of NAT ;
A14: Seg (len (f | i)) = dom (f | i) by FINSEQ_1:def 3;
A15: len (f | i) = i by ;
hence (Card (f | i)) . j = card ((f | i) . j) by
.= card ((f | i) /. j) by
.= card (f /. j) by
.= card (f . j) by
.= (Card f) . j by
.= Cf /. j by
.= (Cf | i) /. j by
.= ((Card f) | i) . j by ;
:: thesis: verum
end;
suppose A16: i > len f ; :: thesis: (Card (f | i)) . b1 = ((Card f) | i) . b1
then f | i = f by ;
hence (Card (f | i)) . j = ((Card f) | i) . j by ; :: thesis: verum
end;
end;
end;
len ((Card f) | i) = min (i,(len (Card f))) by
.= min (i,(len f)) by ;
hence Card (f | i) = (Card f) | i by ; :: thesis: verum