per cases ( V is empty or not V is empty ) ;
suppose V is empty ; :: thesis: ex b1 being FinSequence st
( b1 is one-to-one & b1 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 b1 being FinSequence st
( b1 is one-to-one & b1 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;