let D be non empty set ; :: thesis: for q being FinSequence of D
for n being Nat st NAT c= D & n > len q holds
ex p being XFinSequence of D st
( len p = n & p is_an_xrep_of q )
let q be FinSequence of D; :: thesis: for n being Nat st NAT c= D & n > len q holds
ex p being XFinSequence of D st
( len p = n & p is_an_xrep_of q )
let n be Nat; :: thesis: ( NAT c= D & n > len q implies ex p being XFinSequence of D st
( len p = n & p is_an_xrep_of q ) )
assume that
A1: NAT c= D and
A2: n > len q ; :: thesis: ex p being XFinSequence of D st
( len p = n & p is_an_xrep_of q )
reconsider n = n as Element of NAT by ORDINAL1:def 12;
consider d2 being set such that
A3: d2 in D and
A4: d2 = len q by A1;
reconsider d = d2 as Element of D by A3;
deffunc H₁( object ) -> object = IFEQ ($1,0,d,(IFLGT ($1,(len q),(q . $1),(q . $1),d)));
ex p being XFinSequence st
( len p = n & ( for k being Nat st k in n holds
p . k = H₁(k) ) ) from AFINSQ_1:sch 2();
then consider p being XFinSequence such that
A5: len p = n and
A6: for k being Nat st k in n holds
p . k = H₁(k) ;
rng p c= D

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in D )
assume y in rng p ; :: thesis: y in D
then consider x being object such that
A7: x in dom p and
A8: y = p . x by FUNCT_1:def 3;
reconsider nx = x as Ordinal by A7;
reconsider kx = nx as Element of NAT by A7;
A9: p . kx = H₁(kx) by A5, A6, A7;

now :: thesis: ( ( x = 0 & p . x in D ) or ( x <> 0 & p . x in D ) )

per cases ( x = 0 or x <> 0 ) ;

case x = 0 ; :: thesis: p . x in D

then H₁(x) = d by FUNCOP_1:def 8;
hence p . x in D by A9; :: thesis: verum

end;

case A10: x <> 0 ; :: thesis: p . x in D

then A11: H₁(x) = IFLGT (x,(len q),(q . x),(q . x),d) by FUNCOP_1:def 8;

now :: thesis: ( ( x in Segm (len q) & p . x in D ) or ( x = len q & p . x in D ) or ( not x in len q & not x = len q & p . x in D ) )

per cases ( x in Segm (len q) or x = len q or ( not x in len q & not x = len q ) ) ;

case A12: x in Segm (len q) ; :: thesis: p . x in D

then A13: kx < len q by NAT_1:44;
0 + 1 <= kx by A10, NAT_1:13;
then kx in Seg (len q) by A13, FINSEQ_1:1;
then x in dom q by FINSEQ_1:def 3;
then A14: q . x in rng q by FUNCT_1:def 3;
A15: rng q c= D by FINSEQ_1:def 4;
H₁(x) = q . x by A11, A12, Def2;
hence p . x in D by A9, A14, A15; :: thesis: verum

end;

case A16: x = len q ; :: thesis: p . x in D

0 + 1 <= kx by A10, NAT_1:13;
then kx in Seg (len q) by A16, FINSEQ_1:1;
then x in dom q by FINSEQ_1:def 3;
then A17: q . x in rng q by FUNCT_1:def 3;
A18: rng q c= D by FINSEQ_1:def 4;
H₁(x) = q . x by A11, A16, Def2;
hence p . x in D by A9, A17, A18; :: thesis: verum

end;

case ( not x in len q & not x = len q ) ; :: thesis: p . x in D

then H₁(x) = d by A11, Def2;
hence p . x in D by A9; :: thesis: verum

end;

end;

end;

hence p . x in D ; :: thesis: verum

end;

end;

end;

hence y in D by A8; :: thesis: verum

end;

then reconsider p = p as XFinSequence of D by RELAT_1:def 19;
reconsider p2 = Replace (p,0,d) as XFinSequence of D ;
A19: for i being Nat st 1 <= i & i <= len q holds
p2 . i = q . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len q implies p2 . i = q . i )
assume that
A20: 1 <= i and
A21: i <= len q ; :: thesis: p2 . i = q . i
( i < len q or i = len q ) by A21, XXREAL_0:1;
then A22: ( i in Segm (len q) or i = len q ) by NAT_1:44;
i < n by A2, A21, XXREAL_0:2;
then A23: i in Segm n by NAT_1:44;
i in NAT by ORDINAL1:def 12;
hence p2 . i = p . i by A20, AFINSQ_1:44
.= H₁(i) by A6, A23
.= IFLGT (i,(len q),(q . i),(q . i),d) by A20, FUNCOP_1:def 8
.= q . i by A22, Def2 ;
:: thesis: verum

end;

A24: len p2 = len p by AFINSQ_1:44;
p2 . 0 = len q by A2, A4, A5, AFINSQ_1:44;
then p2 is_an_xrep_of q by A1, A2, A5, A24, A19;
hence ex p being XFinSequence of D st
( len p = n & p is_an_xrep_of q ) by A5, A24; :: thesis: verum