let n be non zero Nat; 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; 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; for k being Nat holds IDEA_P_F (Key,n,k) is FuncSeq-like FinSequence
let k be Nat; 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;
( 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))
;
(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;
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; verum