let n be non zero Nat; :: thesis: for lk being Nat
for Key being Matrix of lk,6,NAT
for k being Nat st k <> 0 holds
IDEA_P_F (Key,n,k) is FuncSequence of MESSAGES , MESSAGES
let lk be Nat; :: thesis: for Key being Matrix of lk,6,NAT
for k being Nat st k <> 0 holds
IDEA_P_F (Key,n,k) is FuncSequence of MESSAGES , MESSAGES
let Key be Matrix of lk,6,NAT; :: thesis: for k being Nat st k <> 0 holds
IDEA_P_F (Key,n,k) is FuncSequence of MESSAGES , MESSAGES
let k be Nat; :: thesis: ( k <> 0 implies IDEA_P_F (Key,n,k) is FuncSequence of MESSAGES , MESSAGES )
A1: k = len (IDEA_P_F (Key,n,k)) by Def17;
assume A2: k <> 0 ; :: thesis: IDEA_P_F (Key,n,k) is FuncSequence of MESSAGES , MESSAGES
then 0 + 1 < k + 1 by XREAL_1:6;
then A3: 1 <= k by NAT_1:13;
0 + 1 < k + 1 by A2, XREAL_1:6;
then 1 <= k by NAT_1:13;
then 1 in Seg (len (IDEA_P_F (Key,n,k))) by A1, FINSEQ_1:1;
then A4: 1 in dom (IDEA_P_F (Key,n,k)) by FINSEQ_1:def 3;
len (IDEA_P_F (Key,n,k)) = k by Def17;
then not IDEA_P_F (Key,n,k) = <*> MESSAGES by A2;
then A5: firstdom (IDEA_P_F (Key,n,k)) = proj1 ((IDEA_P_F (Key,n,k)) . 1) by FUNCT_7:def 6
.= proj1 (IDEA_P ((Line (Key,1)),n)) by A4, Def17
.= dom (IDEA_P ((Line (Key,1)),n))
.= MESSAGES by FUNCT_2:def 1 ;
k = len (IDEA_P_F (Key,n,k)) by Def17;
then k in Seg (len (IDEA_P_F (Key,n,k))) by A3, FINSEQ_1:1;
then A6: k in dom (IDEA_P_F (Key,n,k)) by FINSEQ_1:def 3;
len (IDEA_P_F (Key,n,k)) <> 0 by A2, Def17;
then not IDEA_P_F (Key,n,k) = <*> MESSAGES ;
then lastrng (IDEA_P_F (Key,n,k)) = proj2 ((IDEA_P_F (Key,n,k)) . (len (IDEA_P_F (Key,n,k)))) by FUNCT_7:def 7
.= proj2 ((IDEA_P_F (Key,n,k)) . k) by Def17
.= proj2 (IDEA_P ((Line (Key,k)),n)) by A6, Def17
.= rng (IDEA_P ((Line (Key,k)),n)) ;
then A7: lastrng (IDEA_P_F (Key,n,k)) c= MESSAGES by RELAT_1:def 19;
IDEA_P_F (Key,n,k) is FuncSequence by Th38;
hence IDEA_P_F (Key,n,k) is FuncSequence of MESSAGES , MESSAGES by A7, A5, FUNCT_7:def 9; :: thesis: verum