A2:
for x being object st x in Seg F_{1}() holds

( ( P_{1}[x] implies F_{3}(x) in F_{2}() ) & ( P_{1}[x] implies F_{4}(x) in F_{2}() ) )
by A1;

consider p being Function of (Seg F_{1}()),F_{2}() such that

A3: for x being object st x in Seg F_{1}() holds

( ( P_{1}[x] implies p . x = F_{3}(x) ) & ( P_{1}[x] implies p . x = F_{4}(x) ) )
from FUNCT_2:sch 5(A2);

A4: dom p = Seg F_{1}()
by FUNCT_2:def 1;

then reconsider p = p as FinSequence by FINSEQ_1:def 2;

rng p c= F_{2}()
by RELAT_1:def 19;

then reconsider p = p as FinSequence of F_{2}() by FINSEQ_1:def 4;

take p ; :: thesis: ( len p = F_{1}() & ( for i being Nat st i in Seg F_{1}() holds

( ( P_{1}[i] implies p . i = F_{3}(i) ) & ( P_{1}[i] implies p . i = F_{4}(i) ) ) ) )

F_{1}() is Element of NAT
by ORDINAL1:def 12;

hence ( len p = F_{1}() & ( for i being Nat st i in Seg F_{1}() holds

( ( P_{1}[i] implies p . i = F_{3}(i) ) & ( P_{1}[i] implies p . i = F_{4}(i) ) ) ) )
by A3, A4, FINSEQ_1:def 3; :: thesis: verum

( ( P

consider p being Function of (Seg F

A3: for x being object st x in Seg F

( ( P

A4: dom p = Seg F

then reconsider p = p as FinSequence by FINSEQ_1:def 2;

rng p c= F

then reconsider p = p as FinSequence of F

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

( ( P

F

hence ( len p = F

( ( P