let D be non empty set ; :: thesis: for p being XFinSequence of D st p . 0 = 0 & 0 < len p holds
XFS2FS* p = {}
let p be XFinSequence of D; :: thesis: ( p . 0 = 0 & 0 < len p implies XFS2FS* p = {} )
assume that
A1: p . 0 = 0 and
A2: 0 < len p ; :: thesis: XFS2FS* p = {}
set q = XFS2FS* p;
0 in len p by A2, Lm1;
then len (XFS2FS* p) = 0 by A1, Def11;
hence XFS2FS* p = {} ; :: thesis: verum