take {} ; :: thesis: ( {} is FinSequence-membered & {} is with_common_domain )
thus ( {} is FinSequence-membered & {} is with_common_domain ) ; :: thesis: verum