consider p being FinSequence such that
A1: ( len p = len F1() & ( for i being natural set st i in dom p holds
p . i = F2(i) ) ) from FINSEQ_1:sch 2();
 A2: dom p = dom F1() by A1, FINSEQ_3:29;
reconsider p = p as non empty FinSequence by A1;
take p ; :: thesis: ( dom p = dom F1() & ( for i being Element of dom F1() holds p . i = F2(i) ) )
thus ( dom p = dom F1() & ( for i being Element of dom F1() holds p . i = F2(i) ) ) by A2, A1; :: thesis: verum