scheme :: LOPBAN_4:sch 1
ExNormSpaceCASE{ F₁() -> Banach_Algebra, F₂( Nat, Nat) -> Point of F₁() } :

for k being Nat ex seq being sequence of F₁() st
for n being Nat holds
( ( n <= k implies seq . n = F₂(k,n) ) & ( n > k implies seq . n = 0. F₁() ) )