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;

.= min (i,(len f)) by A4, FINSEQ_3:29 ;

hence Card (f | i) = (Card f) | i by A2, A6, FINSEQ_2:9; :: thesis: verum

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

len ((Card f) | i) =
min (i,(len (Card f)))
by A5, FINSEQ_2:21
(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)) . b_{1} = ((Card f) | i) . b_{1} )

assume A8: j in dom (Card (f | i)) ; :: thesis: (Card (f | i)) . b_{1} = ((Card f) | i) . b_{1}

end;let j be Nat; :: thesis: ( j in dom (Card (f | i)) implies (Card (f | i)) . b

assume A8: j in dom (Card (f | i)) ; :: thesis: (Card (f | i)) . b

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

end;

suppose A9:
i <= len f
; :: thesis: (Card (f | i)) . b_{1} = ((Card f) | i) . b_{1}

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;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

.= min (i,(len f)) by A4, FINSEQ_3:29 ;

hence Card (f | i) = (Card f) | i by A2, A6, FINSEQ_2:9; :: thesis: verum