consider p being FinSequence such that
A1: ( len p = len F₁() & ( for i being Nat st i in dom p holds
p . i = F₂(i) ) ) from FINSEQ_1:sch 2();
reconsider p9 = p as non empty FinSequence by A1;
take p9 ; :: thesis: ( len p9 = len F₁() & ( for i being Element of dom F₁() holds p9 . i = F₂(i) ) )
thus len p9 = len F₁() by A1; :: thesis: for i being Element of dom F₁() holds p9 . i = F₂(i)
let i be Element of dom F₁(); :: thesis: p9 . i = F₂(i)
A2: dom F₁() = Seg (len F₁()) by FINSEQ_1:def 3;
dom p = Seg (len F₁()) by A1, FINSEQ_1:def 3;
hence p9 . i = F₂(i) by A1, A2; :: thesis: verum