consider p being FinSequence such that

A1: ( len p = len F_{1}() & ( for i being Nat st i in dom p holds

p . i = F_{2}(i) ) )
from FINSEQ_1:sch 2();

reconsider p9 = p as non empty FinSequence by A1;

take p9 ; :: thesis: ( len p9 = len F_{1}() & ( for i being Element of dom F_{1}() holds p9 . i = F_{2}(i) ) )

thus len p9 = len F_{1}()
by A1; :: thesis: for i being Element of dom F_{1}() holds p9 . i = F_{2}(i)

let i be Element of dom F_{1}(); :: thesis: p9 . i = F_{2}(i)

A2: dom F_{1}() = Seg (len F_{1}())
by FINSEQ_1:def 3;

dom p = Seg (len F_{1}())
by A1, FINSEQ_1:def 3;

hence p9 . i = F_{2}(i)
by A1, A2; :: thesis: verum

A1: ( len p = len F

p . i = F

reconsider p9 = p as non empty FinSequence by A1;

take p9 ; :: thesis: ( len p9 = len F

thus len p9 = len F

let i be Element of dom F

A2: dom F

dom p = Seg (len F

hence p9 . i = F