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

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