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