theorem Th7: :: FRIENDS1:7

for p being FinSequence st len p is prime & ex i being Nat st
( 0 < i & i < len p & p = (p /^ i) ^ (p | i) ) holds
rng p c= {(p . 1)}