consider p being FinSequence;
take p .--> 0 ; :: thesis: ( not p .--> 0 is empty & p .--> 0 is homogeneous )
thus ( not p .--> 0 is empty & p .--> 0 is homogeneous ) ; :: thesis: verum