let D be non empty set ; :: thesis: for f being FinSequence of D

for n being Nat holds (f | n) ^ (f /^ n) = f

let f be FinSequence of D; :: thesis: for n being Nat holds (f | n) ^ (f /^ n) = f

let n be Nat; :: thesis: (f | n) ^ (f /^ n) = f

set fn = f /^ n;

for n being Nat holds (f | n) ^ (f /^ n) = f

let f be FinSequence of D; :: thesis: for n being Nat holds (f | n) ^ (f /^ n) = f

let n be Nat; :: thesis: (f | n) ^ (f /^ n) = f

set fn = f /^ n;

now :: thesis: ( ( len f < n & (f | n) ^ (f /^ n) = f ) or ( n <= len f & (f | n) ^ (f /^ n) = f ) )end;

hence
(f | n) ^ (f /^ n) = f
; :: thesis: verumper cases
( len f < n or n <= len f )
;

end;

case
len f < n
; :: thesis: (f | n) ^ (f /^ n) = f

then
( f /^ n = <*> D & f | n = f )
by Def1, Lm3;

hence (f | n) ^ (f /^ n) = f by FINSEQ_1:34; :: thesis: verum

end;hence (f | n) ^ (f /^ n) = f by FINSEQ_1:34; :: thesis: verum

case A1:
n <= len f
; :: thesis: (f | n) ^ (f /^ n) = f

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

end;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 :: thesis: for m being Nat st m in dom f holds

((f | n) ^ (f /^ n)) . m = f . m

hence
(f | n) ^ (f /^ n) = f
by A5, FINSEQ_2:9; :: thesis: verum((f | n) ^ (f /^ n)) . m = f . m

let m be Nat; :: thesis: ( m in dom f implies ((f | n) ^ (f /^ n)) . m = f . m )

assume A7: m in dom f ; :: thesis: ((f | n) ^ (f /^ n)) . m = f . m

then A8: m <= len f by A2, FINSEQ_1:1;

A9: 1 <= m by A2, A7, FINSEQ_1:1;

end;assume A7: m in dom f ; :: thesis: ((f | n) ^ (f /^ n)) . m = f . m

then A8: m <= len f by A2, FINSEQ_1:1;

A9: 1 <= m by A2, A7, FINSEQ_1:1;

now :: thesis: ( ( m <= n & ((f | n) ^ (f /^ n)) . m = f . m ) or ( n < m & ((f | n) ^ (f /^ n)) . m = f . m ) )end;

hence
((f | n) ^ (f /^ n)) . m = f . m
; :: thesis: verumper cases
( m <= n or n < m )
;

end;

case A10:
m <= n
; :: thesis: ((f | n) ^ (f /^ n)) . m = f . m

then
1 <= n
by A9, XXREAL_0:2;

then A11: n in dom f by A1, FINSEQ_3:25;

A12: m in Seg n by A9, A10, FINSEQ_1:1;

hence ((f | n) ^ (f /^ n)) . m = (f | n) . m by A6, FINSEQ_1:def 7

.= f . m by A12, A11, Th6 ;

:: thesis: verum

end;then A11: n in dom f by A1, FINSEQ_3:25;

A12: m in Seg n by A9, A10, FINSEQ_1:1;

hence ((f | n) ^ (f /^ n)) . m = (f | n) . m by A6, FINSEQ_1:def 7

.= f . m by A12, A11, Th6 ;

:: thesis: verum

case A13:
n < m
; :: thesis: ((f | n) ^ (f /^ n)) . m = f . m

then
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 ; :: thesis: verum

end;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 ; :: thesis: verum