deffunc H₁( Nat, Nat) -> set = 1 / (($2 !) * (($1 -' $2) !));
for n being Nat ex seq being Real_Sequence st
for k being Nat holds
( ( k <= n implies seq . k = H₁(n,k) ) & ( k > n implies seq . k = 0 ) ) from SIN_COS:sch 2();
hence ex b₁ being Real_Sequence st
for k being Nat holds
( ( k <= n implies b₁ . k = 1 / ((k !) * ((n -' k) !)) ) & ( k > n implies b₁ . k = 0 ) ) ; :: thesis: verum