Theorem LinearIndepOn.singleton'

feat: add an element to a linear indep family, more general version (#31515)