scheme :: LOPBAN_4:sch 1
ExNormSpaceCASE{ F1() -> Banach_Algebra, F2( Nat, Nat) -> Point of F1() } :
for k being Nat ex seq being sequence of F1() st
for n being Nat holds
( ( n <= k implies seq . n = F2(k,n) ) & ( n > k implies seq . n = 0. F1() ) )