let n be non zero Nat; for lk being Nat
for Key being Matrix of lk,6,NAT
for r being Nat holds
( rng (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) c= MESSAGES & dom (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) = MESSAGES )
let lk be Nat; for Key being Matrix of lk,6,NAT
for r being Nat holds
( rng (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) c= MESSAGES & dom (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) = MESSAGES )
let Key be Matrix of lk,6,NAT; for r being Nat holds
( rng (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) c= MESSAGES & dom (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) = MESSAGES )
let r be Nat; ( rng (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) c= MESSAGES & dom (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) = MESSAGES )
A1:
rng (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) c= MESSAGES
proof
per cases
( r <> 0 or r = 0 )
;
suppose A2:
r <> 0
;
rng (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) c= MESSAGES then
0 + 1
< r + 1
by XREAL_1:6;
then A3:
1
<= 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 A3, FINSEQ_1:1;
then A4:
r in dom (IDEA_Q_F (Key,n,r))
by FINSEQ_1:def 3;
len (IDEA_Q_F (Key,n,r)) <> 0
by A2, Def18;
then A5:
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 A4, Def18
.=
rng (IDEA_Q ((Line (Key,((r -' r) + 1))),n))
;
then A6:
lastrng (IDEA_Q_F (Key,n,r)) c= MESSAGES
by RELAT_1:def 19;
rng (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) c= lastrng (IDEA_Q_F (Key,n,r))
by A5, FUNCT_7:59;
hence
rng (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) c= MESSAGES
by A6, XBOOLE_1:1;
verum end; suppose
r = 0
;
rng (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) c= MESSAGES then
len (IDEA_Q_F (Key,n,r)) = 0
by Def18;
then
IDEA_Q_F (
Key,
n,
r)
= {}
;
then
compose (
(IDEA_Q_F (Key,n,r)),
MESSAGES)
= id MESSAGES
by FUNCT_7:39;
hence
rng (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) c= MESSAGES
;
verum end; end;
end;
A7:
IDEA_Q_F (Key,n,r) is FuncSequence
by Th39;
dom (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) = MESSAGES
proof
per cases
( r = 0 or r <> 0 )
;
suppose
r = 0
;
dom (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) = MESSAGES then
len (IDEA_Q_F (Key,n,r)) = 0
by Def18;
then
IDEA_Q_F (
Key,
n,
r)
= {}
;
then
compose (
(IDEA_Q_F (Key,n,r)),
MESSAGES)
= id MESSAGES
by FUNCT_7:39;
hence
dom (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) = MESSAGES
;
verum end; suppose A8:
r <> 0
;
dom (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) = MESSAGES then
0 + 1
< r + 1
by XREAL_1:6;
then A9:
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 A9, FINSEQ_1:1;
then A10:
1
in dom (IDEA_Q_F (Key,n,r))
by FINSEQ_1:def 3;
len (IDEA_Q_F (Key,n,r)) <> 0
by A8, Def18;
then
not
IDEA_Q_F (
Key,
n,
r)
= <*> MESSAGES
;
then 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 A10, Def18
.=
dom (IDEA_Q ((Line (Key,((r -' 1) + 1))),n))
.=
MESSAGES
by FUNCT_2:def 1
;
hence
dom (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) = MESSAGES
by A7, FUNCT_7:62;
verum end; end;
end;
hence
( rng (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) c= MESSAGES & dom (compose ((IDEA_Q_F (Key,n,r)),MESSAGES)) = MESSAGES )
by A1; verum