theorem Th47: :: NUMBER17:47

for f being 3 -element natural-valued positive FinSequence ex a, b, c being positive Nat st f = <*a,b,c*>