let D be non empty set ; :: thesis: for p being non empty XFinSequence of st NAT c= D & p . 0 is Nat & p . 0 in len p holds
p is_an_xrep_of XFS2FS* p
let p be non empty XFinSequence of ; :: thesis: ( NAT c= D & p . 0 is Nat & p . 0 in len p implies p is_an_xrep_of XFS2FS* p )
assume A1: ( NAT c= D & p . 0 is Nat & p . 0 in len p ) ; :: thesis: p is_an_xrep_of XFS2FS* p
then reconsider m0 = p . 0 as Nat ;
A2: ( len (XFS2FS* p) = m0 & ( for i being Nat st 1 <= i & i <= m0 holds
(XFS2FS* p) . i = p . i ) ) by A1, Def4;
A3: m0 < len p by A1, NAT_1:45;
thus p is_an_xrep_of XFS2FS* p by A1, A2, A3, Def5; :: thesis: verum