deffunc H_{1}( 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_{1}(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

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

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