deffunc H₁( Nat) -> Function of MESSAGES ,MESSAGES = IDEA_P (Line Key,$1),n;
consider z being FinSequence such that
A1: ( len z = r & ( for k being Nat st k in dom z holds
z . k = H₁(k) ) ) from FINSEQ_1:sch 2();
take z ; :: thesis: ( len z = r & ( for i being Element of NAT st i in dom z holds
z . i = IDEA_P (Line Key,i),n ) )
thus ( len z = r & ( for i being Element of NAT st i in dom z holds
z . i = IDEA_P (Line Key,i),n ) ) by A1; :: thesis: verum