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

for n being Nat

for x being set st len f = n + 1 & x = f . (n + 1) holds

f = (f | n) ^ <*x*>

let f be FinSequence of D; :: thesis: for n being Nat

for x being set st len f = n + 1 & x = f . (n + 1) holds

f = (f | n) ^ <*x*>

let n be Nat; :: thesis: for x being set st len f = n + 1 & x = f . (n + 1) holds

f = (f | n) ^ <*x*>

let x be set ; :: thesis: ( len f = n + 1 & x = f . (n + 1) implies f = (f | n) ^ <*x*> )

assume that

A1: len f = n + 1 and

A2: x = f . (n + 1) ; :: thesis: f = (f | n) ^ <*x*>

set fn = f | n;

A3: len (f | n) = n by A1, FINSEQ_1:59, NAT_1:11;

A4: dom f = Seg (len f) by FINSEQ_1:def 3;

A5: n <= n + 1 by NAT_1:11;

.= len f by A1, FINSEQ_1:40 ;

hence f = (f | n) ^ <*x*> by A6, FINSEQ_2:9; :: thesis: verum

for n being Nat

for x being set st len f = n + 1 & x = f . (n + 1) holds

f = (f | n) ^ <*x*>

let f be FinSequence of D; :: thesis: for n being Nat

for x being set st len f = n + 1 & x = f . (n + 1) holds

f = (f | n) ^ <*x*>

let n be Nat; :: thesis: for x being set st len f = n + 1 & x = f . (n + 1) holds

f = (f | n) ^ <*x*>

let x be set ; :: thesis: ( len f = n + 1 & x = f . (n + 1) implies f = (f | n) ^ <*x*> )

assume that

A1: len f = n + 1 and

A2: x = f . (n + 1) ; :: thesis: f = (f | n) ^ <*x*>

set fn = f | n;

A3: len (f | n) = n by A1, FINSEQ_1:59, NAT_1:11;

A4: dom f = Seg (len f) by FINSEQ_1:def 3;

A5: n <= n + 1 by NAT_1:11;

A6: now :: thesis: for m being Nat st m in dom f holds

f . m = ((f | n) ^ <*x*>) . m

len ((f | n) ^ <*x*>) =
n + (len <*x*>)
by A3, FINSEQ_1:22
f . m = ((f | n) ^ <*x*>) . m

let m be Nat; :: thesis: ( m in dom f implies f . m = ((f | n) ^ <*x*>) . m )

assume A7: m in dom f ; :: thesis: f . m = ((f | n) ^ <*x*>) . m

then A8: 1 <= m by A4, FINSEQ_1:1;

A9: m <= len f by A4, A7, FINSEQ_1:1;

end;assume A7: m in dom f ; :: thesis: f . m = ((f | n) ^ <*x*>) . m

then A8: 1 <= m by A4, FINSEQ_1:1;

A9: m <= len f by A4, A7, FINSEQ_1:1;

now :: thesis: ( ( m = len f & f . m = ((f | n) ^ <*x*>) . m ) or ( m <> len f & ((f | n) ^ <*x*>) . m = f . m ) )end;

hence
f . m = ((f | n) ^ <*x*>) . m
; :: thesis: verumper cases
( m = len f or m <> len f )
;

end;

case
m <> len f
; :: thesis: ((f | n) ^ <*x*>) . m = f . m

then
m < n + 1
by A1, A9, XXREAL_0:1;

then A10: m <= n by NAT_1:13;

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

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

A12: Seg (len (f | n)) = dom (f | n) by FINSEQ_1:def 3;

A13: m in dom (f | n) by A3, A8, A10, FINSEQ_3:25;

hence ((f | n) ^ <*x*>) . m = (f | n) . m by FINSEQ_1:def 7

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

:: thesis: verum

end;then A10: m <= n by NAT_1:13;

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

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

A12: Seg (len (f | n)) = dom (f | n) by FINSEQ_1:def 3;

A13: m in dom (f | n) by A3, A8, A10, FINSEQ_3:25;

hence ((f | n) ^ <*x*>) . m = (f | n) . m by FINSEQ_1:def 7

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

:: thesis: verum

.= len f by A1, FINSEQ_1:40 ;

hence f = (f | n) ^ <*x*> by A6, FINSEQ_2:9; :: thesis: verum