A2: for x being object st x in Seg F1() holds
( ( P1[x] implies F3(x) in F2() ) & ( P1[x] implies F4(x) in F2() ) ) by A1;
consider p being Function of (Seg F1()),F2() such that
A3: for x being object st x in Seg F1() holds
( ( P1[x] implies p . x = F3(x) ) & ( P1[x] implies p . x = F4(x) ) ) from FUNCT_2:sch 5(A2);
 A4: dom p = Seg F1() by FUNCT_2:def 1;
then reconsider p = p as FinSequence by FINSEQ_1:def 2;
rng p c= F2() by RELAT_1:def 19;
then reconsider p = p as FinSequence of F2() by FINSEQ_1:def 4;
take p ; :: thesis: ( len p = F1() & ( for i being Nat st i in Seg F1() holds
( ( P1[i] implies p . i = F3(i) ) & ( P1[i] implies p . i = F4(i) ) ) ) )
F1() is Element of NAT by ORDINAL1:def 12;
hence ( len p = F1() & ( for i being Nat st i in Seg F1() holds
( ( P1[i] implies p . i = F3(i) ) & ( P1[i] implies p . i = F4(i) ) ) ) ) by A3, A4, FINSEQ_1:def 3; :: thesis: verum