let D be set ; for f being FinSequence of D
for n being Nat holds (f | n) ^ (f /^ n) = f
let f be FinSequence of D; for n being Nat holds (f | n) ^ (f /^ n) = f
let n be Nat; (f | n) ^ (f /^ n) = f
set fn = f /^ n;
per cases
( len f < n or n <= len f )
;
suppose A1:
n <= len f
;
(f | n) ^ (f /^ n) = fthen A3:
len (f | n) = n
by FINSEQ_1:59;
A4:
len (f /^ n) = (len f) - n
by A1, RFINSEQ:def 1;
then A5:
len ((f | n) ^ (f /^ n)) = n + ((len f) - n)
by A3, FINSEQ_1:22;
A6:
dom (f | n) = Seg n
by A3, FINSEQ_1:def 3;
now for m being Nat st m in dom f holds
((f | n) ^ (f /^ n)) . m = f . mlet m be
Nat;
( m in dom f implies ((f | n) ^ (f /^ n)) . b1 = f . b1 )assume
m in dom f
;
((f | n) ^ (f /^ n)) . b1 = f . b1then A8:
( 1
<= m &
m <= len f )
by FINSEQ_3:25;
per cases
( m <= n or n < m )
;
suppose A13:
n < m
;
((f | n) ^ (f /^ n)) . b1 = f . b1then
max (
0,
(m - n))
= m - n
by FINSEQ_2:4;
then reconsider k =
m - n as
Element of
NAT by FINSEQ_2:5;
n + 1
<= m
by A13, NAT_1:13;
then
1
<= k
by XREAL_1:19;
then A15:
k in dom (f /^ n)
by A4, A8, XREAL_1:9, FINSEQ_3:25;
((f | n) ^ (f /^ n)) . m = (f /^ n) . k
by A3, A5, A8, A13, FINSEQ_1:24;
then
((f | n) ^ (f /^ n)) . m = f . (k + n)
by A1, A15, RFINSEQ:def 1;
hence
((f | n) ^ (f /^ n)) . m = f . m
;
verum end; end; end; hence
(f | n) ^ (f /^ n) = f
by A5, FINSEQ_2:9;
verum end; end;