deffunc H_{1}( Nat) -> Real = delta (T . (In ($1,NAT)));

consider IT being Real_Sequence such that

A1: for i being Nat holds IT . i = H_{1}(i)
from SEQ_1:sch 1();

take IT ; :: thesis: for i being Element of NAT holds IT . i = delta (T . i)

let i be Element of NAT ; :: thesis: IT . i = delta (T . i)

IT . i = H_{1}(i)
by A1;

hence IT . i = delta (T . i) ; :: thesis: verum

consider IT being Real_Sequence such that

A1: for i being Nat holds IT . i = H

take IT ; :: thesis: for i being Element of NAT holds IT . i = delta (T . i)

let i be Element of NAT ; :: thesis: IT . i = delta (T . i)

IT . i = H

hence IT . i = delta (T . i) ; :: thesis: verum