deffunc H₂( Nat, Point of X) -> Element of the carrier of X = $2 + (seq . ($1 + 1));
consider f being sequence of the carrier of X such that
A1: ( f . 0 = seq . 0 & ( for n being Nat holds f . (n + 1) = H₂(n,f . n) ) ) from NAT_1:sch 12();
take f ; :: thesis: ( f . 0 = seq . 0 & ( for n being Nat holds f . (n + 1) = (f . n) + (seq . (n + 1)) ) )
thus ( f . 0 = seq . 0 & ( for n being Nat holds f . (n + 1) = (f . n) + (seq . (n + 1)) ) ) by A1; :: thesis: verum