let n be non zero Nat; :: thesis: for lk being Nat
for Key being Matrix of lk,6,NAT
for k being Nat holds IDEA_P_F (Key,n,k) is FuncSeq-like FinSequence
let lk be Nat; :: thesis: for Key being Matrix of lk,6,NAT
for k being Nat holds IDEA_P_F (Key,n,k) is FuncSeq-like FinSequence
let Key be Matrix of lk,6,NAT; :: thesis: for k being Nat holds IDEA_P_F (Key,n,k) is FuncSeq-like FinSequence
let k be Nat; :: thesis: IDEA_P_F (Key,n,k) is FuncSeq-like FinSequence
set p = (Seg (k + 1)) --> MESSAGES;
A1: dom ((Seg (k + 1)) --> MESSAGES) = Seg (k + 1) by FUNCOP_1:13;
reconsider p = (Seg (k + 1)) --> MESSAGES as FinSequence ;
A2: for i being Nat st i in dom (IDEA_P_F (Key,n,k)) holds
(IDEA_P_F (Key,n,k)) . i in Funcs ((p . i),(p . (i + 1)))

proof

let i be Nat; :: thesis: ( i in dom (IDEA_P_F (Key,n,k)) implies (IDEA_P_F (Key,n,k)) . i in Funcs ((p . i),(p . (i + 1))) )
assume A3: i in dom (IDEA_P_F (Key,n,k)) ; :: thesis: (IDEA_P_F (Key,n,k)) . i in Funcs ((p . i),(p . (i + 1)))
then A4: i in Seg (len (IDEA_P_F (Key,n,k))) by FINSEQ_1:def 3;
then i in Seg k by Def17;
then A5: i <= k by FINSEQ_1:1;
then A6: i <= k + 1 by NAT_1:12;
( 1 <= i + 1 & i + 1 <= k + 1 ) by A5, NAT_1:12, XREAL_1:6;
then i + 1 in Seg (k + 1) by FINSEQ_1:1;
then A7: p . (i + 1) = MESSAGES by FUNCOP_1:7;
1 <= i by A4, FINSEQ_1:1;
then i in Seg (k + 1) by A6, FINSEQ_1:1;
then A8: p . i = MESSAGES by FUNCOP_1:7;
(IDEA_P_F (Key,n,k)) . i = IDEA_P ((Line (Key,i)),n) by A3, Def17;
hence (IDEA_P_F (Key,n,k)) . i in Funcs ((p . i),(p . (i + 1))) by A8, A7, FUNCT_2:9; :: thesis: verum

end;

len p = k + 1 by A1, FINSEQ_1:def 3;
then len p = (len (IDEA_P_F (Key,n,k))) + 1 by Def17;
hence IDEA_P_F (Key,n,k) is FuncSeq-like FinSequence by A2, FUNCT_7:def 8; :: thesis: verum