let i be Nat; :: thesis: 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; :: thesis: ( 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) ; :: thesis: (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; :: thesis: verum