defpred S₁[ Nat, FinSequence] means ( len $2 = F₃($1) & ( for n being Element of NAT st n in dom $2 holds
$2 . n = F₄($1,n) ) );
A1: for k being Nat st k in Seg F₂() holds
ex d being Element of F₁() * st S₁[k,d]

proof

let k be Nat; :: thesis: ( k in Seg F₂() implies ex d being Element of F₁() * st S₁[k,d] )
assume k in Seg F₂() ; :: thesis: ex d being Element of F₁() * st S₁[k,d]
deffunc H₁( Nat) -> Element of F₁() = F₄(k,$1);
consider d being FinSequence of F₁() such that
A2: len d = F₃(k) and
A3: for n being Nat st n in dom d holds
d . n = H₁(n) from FINSEQ_2:sch 1();
reconsider d = d as Element of F₁() * by FINSEQ_1:def 11;
take d ; :: thesis: S₁[k,d]
thus len d = F₃(k) by A2; :: thesis: for n being Element of NAT st n in dom d holds
d . n = F₄(k,n)
let n be Element of NAT ; :: thesis: ( n in dom d implies d . n = F₄(k,n) )
assume n in dom d ; :: thesis: d . n = F₄(k,n)
hence d . n = F₄(k,n) by A3; :: thesis: verum

end;

consider p being FinSequence of F₁() * such that
A4: dom p = Seg F₂() and
A5: for k being Nat st k in Seg F₂() holds
S₁[k,p /. k] from RECDEF_1:sch 17(A1);
take p ; :: thesis: ( len p = F₂() & ( for k being Element of NAT st k in Seg F₂() holds
( len (p /. k) = F₃(k) & ( for n being Element of NAT st n in dom (p /. k) holds
(p /. k) . n = F₄(k,n) ) ) ) )
thus len p = F₂() by A4, FINSEQ_1:def 3; :: thesis: for k being Element of NAT st k in Seg F₂() holds
( len (p /. k) = F₃(k) & ( for n being Element of NAT st n in dom (p /. k) holds
(p /. k) . n = F₄(k,n) ) )
let k be Element of NAT ; :: thesis: ( k in Seg F₂() implies ( len (p /. k) = F₃(k) & ( for n being Element of NAT st n in dom (p /. k) holds
(p /. k) . n = F₄(k,n) ) ) )
assume k in Seg F₂() ; :: thesis: ( len (p /. k) = F₃(k) & ( for n being Element of NAT st n in dom (p /. k) holds
(p /. k) . n = F₄(k,n) ) )
hence ( len (p /. k) = F₃(k) & ( for n being Element of NAT st n in dom (p /. k) holds
(p /. k) . n = F₄(k,n) ) ) by A5; :: thesis: verum