let n be non empty Element of NAT ; :: thesis: for lk being Element of NAT
for Key being Matrix of lk,6, NAT
for k being Element of NAT holds IDEA_Q_F Key,n,k is FuncSeq-like FinSequence
let lk be Element of NAT ; :: thesis: for Key being Matrix of lk,6, NAT
for k being Element of NAT holds IDEA_Q_F Key,n,k is FuncSeq-like FinSequence
let Key be Matrix of lk,6, NAT ; :: thesis: for k being Element of NAT holds IDEA_Q_F Key,n,k is FuncSeq-like FinSequence
let k be Element of NAT ; :: thesis: IDEA_Q_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:19;
reconsider p = (Seg (k + 1)) --> MESSAGES as FinSequence ;
A2: for i being Element of NAT st i in dom (IDEA_Q_F Key,n,k) holds
(IDEA_Q_F Key,n,k) . i in Funcs (p . i),(p . (i + 1))

proof

let i be Element of NAT ; :: thesis: ( i in dom (IDEA_Q_F Key,n,k) implies (IDEA_Q_F Key,n,k) . i in Funcs (p . i),(p . (i + 1)) )
assume A3: i in dom (IDEA_Q_F Key,n,k) ; :: thesis: (IDEA_Q_F Key,n,k) . i in Funcs (p . i),(p . (i + 1))
then A4: i in Seg (len (IDEA_Q_F Key,n,k)) by FINSEQ_1:def 3;
then i in Seg k by Def18;
then A5: i <= k by FINSEQ_1:3;
then A6: i <= k + 1 by NAT_1:12;
( 1 <= i + 1 & i + 1 <= k + 1 ) by A5, NAT_1:12, XREAL_1:8;
then i + 1 in Seg (k + 1) by FINSEQ_1:3;
then A7: p . (i + 1) = MESSAGES by FUNCOP_1:13;
1 <= i by A4, FINSEQ_1:3;
then i in Seg (k + 1) by A6, FINSEQ_1:3;
then A8: p . i = MESSAGES by FUNCOP_1:13;
(IDEA_Q_F Key,n,k) . i = IDEA_Q (Line Key,((k -' i) + 1)),n by A3, Def18;
hence (IDEA_Q_F Key,n,k) . i in Funcs (p . i),(p . (i + 1)) by A8, A7, FUNCT_2:12; :: thesis: verum

end;

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