let n be non zero Nat; :: thesis: for lk being Nat
for Key being Matrix of lk,6,NAT
for r being Nat holds
( rng (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) c= MESSAGES & dom (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) = MESSAGES )
let lk be Nat; :: thesis: for Key being Matrix of lk,6,NAT
for r being Nat holds
( rng (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) c= MESSAGES & dom (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) = MESSAGES )
let Key be Matrix of lk,6,NAT; :: thesis: for r being Nat holds
( rng (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) c= MESSAGES & dom (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) = MESSAGES )
let r be Nat; :: thesis: ( rng (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) c= MESSAGES & dom (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) = MESSAGES )
A1: rng (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) c= MESSAGES

proof

per cases ( r <> 0 or r = 0 ) ;

suppose A2: r <> 0 ; :: thesis: rng (compose ((IDEA_P_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_P_F (Key,n,r)) by Def17;
then r in Seg (len (IDEA_P_F (Key,n,r))) by A3, FINSEQ_1:1;
then A4: r in dom (IDEA_P_F (Key,n,r)) by FINSEQ_1:def 3;
len (IDEA_P_F (Key,n,r)) <> 0 by A2, Def17;
then A5: not IDEA_P_F (Key,n,r) = <*> MESSAGES ;
then lastrng (IDEA_P_F (Key,n,r)) = proj2 ((IDEA_P_F (Key,n,r)) . (len (IDEA_P_F (Key,n,r)))) by FUNCT_7:def 7
.= proj2 ((IDEA_P_F (Key,n,r)) . r) by Def17
.= proj2 (IDEA_P ((Line (Key,r)),n)) by A4, Def17
.= rng (IDEA_P ((Line (Key,r)),n)) ;
then A6: lastrng (IDEA_P_F (Key,n,r)) c= MESSAGES by RELAT_1:def 19;
rng (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) c= lastrng (IDEA_P_F (Key,n,r)) by A5, FUNCT_7:59;
hence rng (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) c= MESSAGES by A6, XBOOLE_1:1; :: thesis: verum

end;

suppose r = 0 ; :: thesis: rng (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) c= MESSAGES

then len (IDEA_P_F (Key,n,r)) = 0 by Def17;
then IDEA_P_F (Key,n,r) = {} ;
then compose ((IDEA_P_F (Key,n,r)),MESSAGES) = id MESSAGES by FUNCT_7:39;
hence rng (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) c= MESSAGES ; :: thesis: verum

end;

end;

end;

A7: IDEA_P_F (Key,n,r) is FuncSequence by Th38;
dom (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) = MESSAGES

proof

per cases ( r = 0 or r <> 0 ) ;

suppose r = 0 ; :: thesis: dom (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) = MESSAGES

then len (IDEA_P_F (Key,n,r)) = 0 by Def17;
then IDEA_P_F (Key,n,r) = {} ;
then compose ((IDEA_P_F (Key,n,r)),MESSAGES) = id MESSAGES by FUNCT_7:39;
hence dom (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) = MESSAGES ; :: thesis: verum

end;

suppose A8: r <> 0 ; :: thesis: dom (compose ((IDEA_P_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_P_F (Key,n,r)) by Def17;
then 1 in Seg (len (IDEA_P_F (Key,n,r))) by A9, FINSEQ_1:1;
then A10: 1 in dom (IDEA_P_F (Key,n,r)) by FINSEQ_1:def 3;
len (IDEA_P_F (Key,n,r)) <> 0 by A8, Def17;
then not IDEA_P_F (Key,n,r) = <*> MESSAGES ;
then firstdom (IDEA_P_F (Key,n,r)) = proj1 ((IDEA_P_F (Key,n,r)) . 1) by FUNCT_7:def 6
.= proj1 (IDEA_P ((Line (Key,1)),n)) by A10, Def17
.= dom (IDEA_P ((Line (Key,1)),n))
.= MESSAGES by FUNCT_2:def 1 ;
hence dom (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) = MESSAGES by A7, FUNCT_7:62; :: thesis: verum

end;

end;

end;

hence ( rng (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) c= MESSAGES & dom (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) = MESSAGES ) by A1; :: thesis: verum