let i be Nat; for f, g, h being FinSequence st len g = len h & len g < i & i <= len (g ^ f) holds
(g ^ f) . i = (h ^ f) . i
let f, g, h be FinSequence; ( len g = len h & len g < i & i <= len (g ^ f) implies (g ^ f) . i = (h ^ f) . i )
assume that
A1:
len g = len h
and
A2:
len g < i
and
A3:
i <= len (g ^ f)
; (g ^ f) . i = (h ^ f) . i
i <= (len g) + (len f)
by A3, FINSEQ_1:22;
then A4:
i - (len g) <= ((len g) + (len f)) - (len g)
by XREAL_1:9;
set k = i - (len g);
A5:
(len g) - (len g) < i - (len g)
by A2, XREAL_1:9;
then reconsider k = i - (len g) as Element of NAT by INT_1:3;
0 + 1 <= i - (len g)
by A5, INT_1:7;
then A6:
k in dom f
by A4, FINSEQ_3:25;
(g ^ f) . i =
(g ^ f) . (k + (len g))
.=
f . k
by A6, FINSEQ_1:def 7
.=
(h ^ f) . ((len h) + k)
by A6, FINSEQ_1:def 7
;
hence
(g ^ f) . i = (h ^ f) . i
by A1; verum