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 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 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 ; :: 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