set p = the FinSequence;
take the FinSequence .--> 0 ; :: thesis: ( not the FinSequence .--> 0 is empty & the FinSequence .--> 0 is homogeneous )
thus ( not the FinSequence .--> 0 is empty & the FinSequence .--> 0 is homogeneous ) ; :: thesis: verum