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