:: deftheorem Def1 defines Cart4Id NUMBER17:def 1 :
for b₁ being Function of NATPLUS,[:NATPLUS,NATPLUS,NATPLUS,NATPLUS:] holds
( b₁ = Cart4Id iff for n being positive Nat holds b₁ . n = [n,n,n,n] );