let D be non empty set ; :: thesis: for p being 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 XFinSequence of ; :: thesis: ( NAT c= D & p . 0 is Nat & p . 0 in len p implies p is_an_xrep_of XFS2FS* p )
assume that
A1: NAT c= D and
A2: p . 0 is Nat and
A3: p . 0 in len p ; :: thesis: p is_an_xrep_of XFS2FS* p
reconsider m0 = p . 0 as Nat by A2;
A4: m0 < len p by A3, NAT_1:44;
( len (XFS2FS* p) = m0 & ( for i being Nat st 1 <= i & i <= m0 holds
(XFS2FS* p) . i = p . i ) ) by A3, AFINSQ_1:def 11;
hence p is_an_xrep_of XFS2FS* p by A1, A4, Def5; :: thesis: verum