let p be Element of PL-WFF ; :: thesis: p is FinSequence-like
PL-WFF c= NAT * by Def5;
hence p is FinSequence-like ; :: thesis: verum