deffunc H₁( Nat, object ) -> Element of REAL = In ((1 / (SquarefreePart ($1 + 1))),REAL);
deffunc H₂() -> Element of REAL = In (0,REAL);
consider f being sequence of REAL such that
A1: ( f . 0 = H₂() & ( for n being Nat holds f . (n + 1) = H₁(n,f . n) ) ) from NAT_1:sch 12();
reconsider f = f as Real_Sequence ;
take f ; :: thesis: ( f . 0 = 0 & ( for i being non zero Nat holds f . i = 1 / (SquarefreePart i) ) )
thus f . 0 = 0 by A1; :: thesis: for i being non zero Nat holds f . i = 1 / (SquarefreePart i)
let n be non zero Nat; :: thesis: f . n = 1 / (SquarefreePart n)
consider k being Nat such that
A2: k + 1 = n by NAT_1:6;
f . (k + 1) = H₁(k,f . k) by A1
.= 1 / (SquarefreePart (k + 1)) ;
hence f . n = 1 / (SquarefreePart n) by A2; :: thesis: verum