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