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
A2:
IDEA_Q_F Key,n,r is FuncSequence
by Th40;
A3:
lastrng (IDEA_Q_F Key,n,r) c= MESSAGES
proof
0 < r
by A1;
then
0 + 1
< r + 1
by XREAL_1:8;
then A4:
( 1
<= r &
r <= r )
by NAT_1:13;
r = len (IDEA_Q_F Key,n,r)
by Def18;
then
r in Seg (len (IDEA_Q_F Key,n,r))
by A4, FINSEQ_1:3;
then A5:
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 A5, Def18
.=
rng (IDEA_Q (Line Key,((r -' r) + 1)),n)
;
hence
lastrng (IDEA_Q_F Key,n,r) c= MESSAGES
by RELSET_1:12;
:: thesis: verum
end;
firstdom (IDEA_Q_F Key,n,r) = MESSAGES
proof
0 < r
by A1;
then
0 + 1
< r + 1
by XREAL_1:8;
then A6:
( 1
<= 1 & 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 A6, FINSEQ_1:3;
then A7:
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
;
hence 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 A7, Def18
.=
dom (IDEA_Q (Line Key,((r -' 1) + 1)),n)
.=
MESSAGES
by FUNCT_2:def 1
;
:: thesis: verum
end;
hence
IDEA_Q_F Key,n,r is FuncSequence of MESSAGES , MESSAGES
by A2, A3, FUNCT_7:def 9; :: thesis: verum