let D be non empty set ; :: thesis: for p being non empty XFinSequence of D 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 D; :: 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:45;
( len (XFS2FS* p) = m0 & ( for i being Nat st 1 <= i & i <= m0 holds
(XFS2FS* p) . i = p . i ) ) by A3, Def4;
hence p is_an_xrep_of XFS2FS* p by A1, A4, Def5; :: thesis: verum