let D be non empty set ; :: thesis: for p being non empty XFinSequence of st NAT c= D & p . 0 = 0 & 0 < len p holds
XFS2FS* p = {}
let p be non empty XFinSequence of ; :: thesis: ( NAT c= D & p . 0 = 0 & 0 < len p implies XFS2FS* p = {} )
assume A1: ( NAT c= D & p . 0 = 0 & 0 < len p ) ; :: thesis: XFS2FS* p = {}
then A2: 0 in len p by NAT_1:45;
set q = XFS2FS* p;
len (XFS2FS* p) = 0 by A1, A2, Def4;
then XFS2FS* p = <*> D by FINSEQ_1:32;
hence XFS2FS* p = {} ; :: thesis: verum