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_Q_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_Q_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_Q_F Key,n,k is FuncSequence of MESSAGES , MESSAGES
let r be Element of 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:8;
then A2: 1 <= r by NAT_1:13;
0 + 1 < r + 1 by A1, XREAL_1:8;
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:3;
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:3;
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 Th40;
hence IDEA_Q_F Key,n,r is FuncSequence of MESSAGES , MESSAGES by A7, A5, FUNCT_7:def 9; :: thesis: verum