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_Q_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_Q_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_Q_F (Key,n,k) is FuncSequence of MESSAGES , MESSAGES
let r be Nat; :: thesis: ( r <> 0 implies IDEA_Q_F (Key,n,r) is FuncSequence of MESSAGES , MESSAGES )
assume A1: r <> 0 ; :: thesis: IDEA_Q_F (Key,n,r) is FuncSequence of MESSAGES , MESSAGES
then 0 + 1 < r + 1 by XREAL_1:6;
then A2: 1 <= r by NAT_1:13;
0 + 1 < r + 1 by A1, XREAL_1:6;
then A3: 1 <= r by NAT_1:13;
r = len (IDEA_Q_F (Key,n,r)) by Def18;
then 1 in Seg (len (IDEA_Q_F (Key,n,r))) by A3, FINSEQ_1:1;
then A4: 1 in dom (IDEA_Q_F (Key,n,r)) by FINSEQ_1:def 3;
len (IDEA_Q_F (Key,n,r)) <> 0 by A1, Def18;
then not IDEA_Q_F (Key,n,r) = <*> MESSAGES ;
then A5: firstdom (IDEA_Q_F (Key,n,r)) = proj1 ((IDEA_Q_F (Key,n,r)) . 1) by FUNCT_7:def 6
.= proj1 (IDEA_Q ((Line (Key,((r -' 1) + 1))),n)) by A4, Def18
.= dom (IDEA_Q ((Line (Key,((r -' 1) + 1))),n))
.= MESSAGES by FUNCT_2:def 1 ;
r = len (IDEA_Q_F (Key,n,r)) by Def18;
then r in Seg (len (IDEA_Q_F (Key,n,r))) by A2, FINSEQ_1:1;
then A6: r in dom (IDEA_Q_F (Key,n,r)) by FINSEQ_1:def 3;
len (IDEA_Q_F (Key,n,r)) <> 0 by A1, Def18;
then not IDEA_Q_F (Key,n,r) = <*> MESSAGES ;
then lastrng (IDEA_Q_F (Key,n,r)) = proj2 ((IDEA_Q_F (Key,n,r)) . (len (IDEA_Q_F (Key,n,r)))) by FUNCT_7:def 7
.= proj2 ((IDEA_Q_F (Key,n,r)) . r) by Def18
.= proj2 (IDEA_Q ((Line (Key,((r -' r) + 1))),n)) by A6, Def18
.= rng (IDEA_Q ((Line (Key,((r -' r) + 1))),n)) ;
then A7: lastrng (IDEA_Q_F (Key,n,r)) c= MESSAGES by RELAT_1:def 19;
IDEA_Q_F (Key,n,r) is FuncSequence by Th39;
hence IDEA_Q_F (Key,n,r) is FuncSequence of MESSAGES , MESSAGES by A7, A5, FUNCT_7:def 9; :: thesis: verum