let D be non empty 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;
now ( ( len f < n & (f | n) ^ (f /^ n) = f ) or ( n <= len f & (f | n) ^ (f /^ n) = f ) )per cases
( len f < n or n <= len f )
;
case A1:
n <= len f
;
(f | n) ^ (f /^ n) = fA2:
dom f = Seg (len f)
by FINSEQ_1:def 3;
A3:
len (f | n) = n
by A1, FINSEQ_1:59;
A4:
len (f /^ n) = (len f) - n
by A1, Def1;
then A5:
len ((f | n) ^ (f /^ n)) =
n + ((len f) - n)
by A3, FINSEQ_1:22
.=
len f
;
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)) . m = f . m )assume A7:
m in dom f
;
((f | n) ^ (f /^ n)) . m = f . mthen A8:
m <= len f
by A2, FINSEQ_1:1;
A9:
1
<= m
by A2, A7, FINSEQ_1:1;
now ( ( m <= n & ((f | n) ^ (f /^ n)) . m = f . m ) or ( n < m & ((f | n) ^ (f /^ n)) . m = f . m ) )per cases
( m <= n or n < m )
;
case A13:
n < m
;
((f | n) ^ (f /^ n)) . m = f . mthen
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 A14:
1
<= k
by XREAL_1:19;
k <= len (f /^ n)
by A4, A8, XREAL_1:9;
then A15:
k in dom (f /^ n)
by A14, FINSEQ_3:25;
thus ((f | n) ^ (f /^ n)) . m =
(f /^ n) . k
by A3, A5, A8, A13, FINSEQ_1:24
.=
f . (k + n)
by A1, A15, Def1
.=
f . m
;
verum end; end; end; hence
((f | n) ^ (f /^ n)) . m = f . m
;
verum end; hence
(f | n) ^ (f /^ n) = f
by A5, FINSEQ_2:9;
verum end; end; end;
hence
(f | n) ^ (f /^ n) = f
; verum