deffunc H₁( Nat) -> Element of K10(X) = (F1 . $1) ` ;
consider f being FinSequence of bool X such that
A1: ( len f = len F1 & ( for n being Nat st n in dom f holds
f . n = H<sub>1</sub>(n) ) ) from FINSEQ_2:sch 1();
take f ; :: thesis: ( len f = len F1 & ( for n being Nat st n in dom f holds
f . n = (F1 . n) ` ) )
thus ( len f = len F1 & ( for n being Nat st n in dom f holds
f . n = (F1 . n) ` ) ) by A1; :: thesis: verum