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 A1, FINSEQ_2:21 ;
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 A4, FINSEQ_3:29;
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 A3, A8, FINSEQ_1:1;
A11: k = i by A9, XXREAL_0:def 9;
then j <= i by A3, A8, FINSEQ_1:1;
then j <= len f by A9, XXREAL_0:2;
then A12: j in dom f by A10, FINSEQ_3:25;
len ((Card f) | i) = i by A7, A9, FINSEQ_1:59;
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:59;
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 6
.= card (f /. j) by A3, A8, A11, A15, A14, FINSEQ_4:70
.= card (f . j) by A12, PARTFUN1:def 6
.= (Card f) . j by A12, CARD_3:def 2
.= Cf /. j by A4, A12, PARTFUN1:def 6
.= (Cf | i) /. j by A3, A8, A11, A13, FINSEQ_4:70
.= ((Card f) | i) . j by A3, A8, A11, A13, PARTFUN1:def 6 ;
:: thesis: verum
end;
suppose A16: i > len f ; :: thesis: (Card (f | i)) . b1 = ((Card f) | i) . b1
then f | i = f by A1, FINSEQ_2:20;
hence (Card (f | i)) . j = ((Card f) | i) . j by A5, A7, A16, FINSEQ_2:20; :: thesis: verum
end;
end;
end;
len ((Card f) | i) = min (i,(len (Card f))) by A5, FINSEQ_2:21
.= min (i,(len f)) by A4, FINSEQ_3:29 ;
hence Card (f | i) = (Card f) | i by A2, A6, FINSEQ_2:9; :: thesis: verum