let n be non empty Element of NAT ; :: thesis: for lk being Element of NAT
for Key being Matrix of lk,6, NAT
for r being Element of 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 Element of NAT ; :: thesis: for Key being Matrix of lk,6, NAT
for r being Element of 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 Element of 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 Element of 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:8;
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:3;
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:61;
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:41;
hence rng (compose (IDEA_P_F Key,n,r),MESSAGES ) c= MESSAGES by RELAT_1:def 19; :: thesis: verum

end;

end;

end;

A7: IDEA_P_F Key,n,r is FuncSequence by Th39;
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:41;
hence dom (compose (IDEA_P_F Key,n,r),MESSAGES ) = MESSAGES by FUNCT_2:67; :: 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:8;
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:3;
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:64; :: 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