per cases ( V is empty or not V is empty ) ;

suppose V is empty ; :: thesis: ex b₁ being FinSequence st
( b₁ is one-to-one & b₁ is V -valued )

take <*> V ; :: thesis: ( <*> V is one-to-one & <*> V is V -valued )
thus ( <*> V is one-to-one & <*> V is V -valued ) ; :: thesis: verum

end;

suppose not V is empty ; :: thesis: ex b₁ being FinSequence st
( b₁ is one-to-one & b₁ is V -valued )

then reconsider V = V as non empty set ;
take <* the Element of V*> ; :: thesis: ( <* the Element of V*> is one-to-one & <* the Element of V*> is V -valued )
thus ( <* the Element of V*> is one-to-one & <* the Element of V*> is V -valued ) ; :: thesis: verum

end;

end;