defpred S_{1}[ Nat, FinSequence] means ( len $2 = F_{3}($1) & ( for n being Element of NAT st n in dom $2 holds

$2 . n = F_{4}($1,n) ) );

A1: for k being Nat st k in Seg F_{2}() holds

ex d being Element of F_{1}() * st S_{1}[k,d]
_{1}() * such that

A4: dom p = Seg F_{2}()
and

A5: for k being Nat st k in Seg F_{2}() holds

S_{1}[k,p /. k]
from RECDEF_1:sch 17(A1);

take p ; :: thesis: ( len p = F_{2}() & ( for k being Element of NAT st k in Seg F_{2}() holds

( len (p /. k) = F_{3}(k) & ( for n being Element of NAT st n in dom (p /. k) holds

(p /. k) . n = F_{4}(k,n) ) ) ) )

thus len p = F_{2}()
by A4, FINSEQ_1:def 3; :: thesis: for k being Element of NAT st k in Seg F_{2}() holds

( len (p /. k) = F_{3}(k) & ( for n being Element of NAT st n in dom (p /. k) holds

(p /. k) . n = F_{4}(k,n) ) )

let k be Element of NAT ; :: thesis: ( k in Seg F_{2}() implies ( len (p /. k) = F_{3}(k) & ( for n being Element of NAT st n in dom (p /. k) holds

(p /. k) . n = F_{4}(k,n) ) ) )

assume k in Seg F_{2}()
; :: thesis: ( len (p /. k) = F_{3}(k) & ( for n being Element of NAT st n in dom (p /. k) holds

(p /. k) . n = F_{4}(k,n) ) )

hence ( len (p /. k) = F_{3}(k) & ( for n being Element of NAT st n in dom (p /. k) holds

(p /. k) . n = F_{4}(k,n) ) )
by A5; :: thesis: verum

$2 . n = F

A1: for k being Nat st k in Seg F

ex d being Element of F

proof

consider p being FinSequence of F
let k be Nat; :: thesis: ( k in Seg F_{2}() implies ex d being Element of F_{1}() * st S_{1}[k,d] )

assume k in Seg F_{2}()
; :: thesis: ex d being Element of F_{1}() * st S_{1}[k,d]

deffunc H_{1}( Nat) -> Element of F_{1}() = F_{4}(k,$1);

consider d being FinSequence of F_{1}() such that

A2: len d = F_{3}(k)
and

A3: for n being Nat st n in dom d holds

d . n = H_{1}(n)
from FINSEQ_2:sch 1();

reconsider d = d as Element of F_{1}() * by FINSEQ_1:def 11;

take d ; :: thesis: S_{1}[k,d]

thus len d = F_{3}(k)
by A2; :: thesis: for n being Element of NAT st n in dom d holds

d . n = F_{4}(k,n)

let n be Element of NAT ; :: thesis: ( n in dom d implies d . n = F_{4}(k,n) )

assume n in dom d ; :: thesis: d . n = F_{4}(k,n)

hence d . n = F_{4}(k,n)
by A3; :: thesis: verum

end;assume k in Seg F

deffunc H

consider d being FinSequence of F

A2: len d = F

A3: for n being Nat st n in dom d holds

d . n = H

reconsider d = d as Element of F

take d ; :: thesis: S

thus len d = F

d . n = F

let n be Element of NAT ; :: thesis: ( n in dom d implies d . n = F

assume n in dom d ; :: thesis: d . n = F

hence d . n = F

A4: dom p = Seg F

A5: for k being Nat st k in Seg F

S

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

( len (p /. k) = F

(p /. k) . n = F

thus len p = F

( len (p /. k) = F

(p /. k) . n = F

let k be Element of NAT ; :: thesis: ( k in Seg F

(p /. k) . n = F

assume k in Seg F

(p /. k) . n = F

hence ( len (p /. k) = F

(p /. k) . n = F