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 st k <> 0 holds
IDEA_P_F Key,n,k is FuncSequence of MESSAGES , MESSAGES
let lk be Element of NAT ; :: thesis: for Key being Matrix of lk,6, NAT
for k being Element of 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 Element of NAT st k <> 0 holds
IDEA_P_F Key,n,k is FuncSequence of MESSAGES , MESSAGES
let k be Element of 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:8;
then A3: 1 <= k by NAT_1:13;
0 + 1 < k + 1 by A2, XREAL_1:8;
then 1 <= k by NAT_1:13;
then 1 in Seg (len (IDEA_P_F Key,n,k)) by A1, FINSEQ_1:3;
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:3;
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 Th39;
hence IDEA_P_F Key,n,k is FuncSequence of MESSAGES , MESSAGES by A7, A5, FUNCT_7:def 9; :: thesis: verum