take <*> Fml ; :: thesis: <*> Fml is FinSequence of Fml
thus <*> Fml is FinSequence of Fml ; :: thesis: verum