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 Nat st i in dom z holds
z . i = IDEA_P ((Line (Key,i)),n) ) )
thus ( len z = r & ( for i being Nat st i in dom z holds
z . i = IDEA_P ((Line (Key,i)),n) ) ) by A1; :: thesis: verum