let D be set ; :: thesis: for f being FinSequence of D *
for i being Element of NAT holds Card (f | i) = (Card f) | i
let f be FinSequence of D * ; :: thesis: for i being Element of NAT holds Card (f | i) = (Card f) | i
let i be Element of 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 Element of NAT by FINSEQ_2: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:31
.= min i,(len f) by A1, FINSEQ_2:24 ;
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

A7: len f = len (Card f) by A4, FINSEQ_3:31;
let j be Nat; :: thesis: ( j in dom (Card (f | i)) implies (Card (f | i)) . b₁ = ((Card f) | i) . b₁ )
assume A8: j in dom (Card (f | i)) ; :: thesis: (Card (f | i)) . b₁ = ((Card f) | i) . b₁

per cases ( i <= len f or i > len f ) ;

suppose A9: i <= len f ; :: thesis: (Card (f | i)) . b₁ = ((Card f) | i) . b₁

A10: 1 <= j by A3, A8, FINSEQ_1:3;
A11: k = i by A9, XXREAL_0:def 9;
then j <= i by A3, A8, FINSEQ_1:3;
then j <= len f by A9, XXREAL_0:2;
then A12: j in dom f by A10, FINSEQ_3:27;
len ((Card f) | i) = i by A7, A9, FINSEQ_1:80;
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 A9, FINSEQ_1:80;
hence (Card (f | i)) . j = card ((f | i) . j) by A3, A8, A11, A14, CARD_3:def 2
.= card ((f | i) /. j) by A3, A8, A11, A15, A14, PARTFUN1:def 8
.= card (f /. j) by A3, A8, A11, A15, A14, FINSEQ_4:85
.= card (f . j) by A12, PARTFUN1:def 8
.= (Card f) . j by A12, CARD_3:def 2
.= Cf /. j by A4, A12, PARTFUN1:def 8
.= (Cf | i) /. j by A3, A8, A11, A13, FINSEQ_4:85
.= ((Card f) | i) . j by A3, A8, A11, A13, PARTFUN1:def 8 ;
:: thesis: verum

end;

suppose A16: i > len f ; :: thesis: (Card (f | i)) . b₁ = ((Card f) | i) . b₁

then f | i = f by A1, FINSEQ_2:23;
hence (Card (f | i)) . j = ((Card f) | i) . j by A5, A7, A16, FINSEQ_2:23; :: thesis: verum

end;

end;

end;

len ((Card f) | i) = min i,(len (Card f)) by A5, FINSEQ_2:24
.= min i,(len f) by A4, FINSEQ_3:31 ;
hence Card (f | i) = (Card f) | i by A2, A6, FINSEQ_2:10; :: thesis: verum