defpred S1[ Nat, FinSequence] means ( len $2 = F3($1) & ( for n being Element of NAT st n in dom $2 holds
$2 . n = F4($1,n) ) );
A1: for k being Nat st k in Seg F2() holds
ex d being Element of F1() * st S1[k,d]
proof
let k be Nat; :: thesis: ( k in Seg F2() implies ex d being Element of F1() * st S1[k,d] )
assume k in Seg F2() ; :: thesis: ex d being Element of F1() * st S1[k,d]
deffunc H1( Nat) -> Element of F1() = F4(k,$1);
consider d being FinSequence of F1() such that
A2: len d = F3(k) and
A3: for n being Nat st n in dom d holds
d . n = H1(n) from FINSEQ_2:sch 1();
 reconsider d = d as Element of F1() * by FINSEQ_1:def 11;
take d ; :: thesis: S1[k,d]
thus len d = F3(k) by A2; :: thesis: for n being Element of NAT st n in dom d holds
d . n = F4(k,n)
let n be Element of NAT ; :: thesis: ( n in dom d implies d . n = F4(k,n) )
assume n in dom d ; :: thesis: d . n = F4(k,n)
hence d . n = F4(k,n) by A3; :: thesis: verum
end;
consider p being FinSequence of F1() * such that
A4: dom p = Seg F2() and
A5: for k being Nat st k in Seg F2() holds
S1[k,p /. k] from RECDEF_1:sch 17(A1);
 take p ; :: thesis: ( len p = F2() & ( for k being Element of NAT st k in Seg F2() holds
( len (p /. k) = F3(k) & ( for n being Element of NAT st n in dom (p /. k) holds
(p /. k) . n = F4(k,n) ) ) ) )
thus len p = F2() by A4, FINSEQ_1:def 3; :: thesis: for k being Element of NAT st k in Seg F2() holds
( len (p /. k) = F3(k) & ( for n being Element of NAT st n in dom (p /. k) holds
(p /. k) . n = F4(k,n) ) )
let k be Element of NAT ; :: thesis: ( k in Seg F2() implies ( len (p /. k) = F3(k) & ( for n being Element of NAT st n in dom (p /. k) holds
(p /. k) . n = F4(k,n) ) ) )
assume k in Seg F2() ; :: thesis: ( len (p /. k) = F3(k) & ( for n being Element of NAT st n in dom (p /. k) holds
(p /. k) . n = F4(k,n) ) )
hence ( len (p /. k) = F3(k) & ( for n being Element of NAT st n in dom (p /. k) holds
(p /. k) . n = F4(k,n) ) ) by A5; :: thesis: verum