take the V8() Real_Sequence ; :: thesis: the V8() Real_Sequence is constant
thus the V8() Real_Sequence is constant ; :: thesis: verum