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, NAT_1:44;
then len (XFS2FS* p) = 0 by A1, Def12;
then XFS2FS* p = <*> D ;
hence XFS2FS* p = {} ; :: thesis: verum