let i be Nat; :: thesis: for f, g being FinSequence st 1 <= i & i <= len f holds
f . i = (g ^ f) . ((len g) + i)
let f, g be FinSequence; :: thesis: ( 1 <= i & i <= len f implies f . i = (g ^ f) . ((len g) + i) )
assume ( 1 <= i & i <= len f ) ; :: thesis: f . i = (g ^ f) . ((len g) + i)
then i in dom f by FINSEQ_3:25;
hence f . i = (g ^ f) . ((len g) + i) by FINSEQ_1:def 7; :: thesis: verum