deffunc H_{1}( Element of NAT ) -> Event of = (A1 . $1) ` ;

consider f being sequence of (bool X) such that

A1: for x being Element of NAT holds f . x = H_{1}(x)
from FUNCT_2:sch 4();

A2: for x being Nat holds f . x = (A1 . x) `

thus for n being Nat holds f . n = (A1 . n) ` by A2; :: thesis: verum

consider f being sequence of (bool X) such that

A1: for x being Element of NAT holds f . x = H

A2: for x being Nat holds f . x = (A1 . x) `

proof

take
f
; :: thesis: for n being Nat holds f . n = (A1 . n) `
let x be Nat; :: thesis: f . x = (A1 . x) `

reconsider x = x as Element of NAT by ORDINAL1:def 12;

f . x = H_{1}(x)
by A1;

hence f . x = (A1 . x) ` ; :: thesis: verum

end;reconsider x = x as Element of NAT by ORDINAL1:def 12;

f . x = H

hence f . x = (A1 . x) ` ; :: thesis: verum

thus for n being Nat holds f . n = (A1 . n) ` by A2; :: thesis: verum