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 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 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 st
( len p = n & p is_an_xrep_of q ) )
assume A1: ( NAT c= D & n > len q ) ; :: thesis: ex p being XFinSequence of st
( len p = n & p is_an_xrep_of q )
reconsider n = n as Element of NAT by ORDINAL1:def 13;
len q in NAT ;
then consider d2 being set such that
A2: ( d2 in D & d2 = len q ) by A1;
reconsider d = d2 as Element of D by A2;
deffunc H₁( set ) -> set = IFEQ $1,0 ,d,(IFLGT $1,(len q),(q . $1),(q . $1),d);
ex p being XFinSequence st
( len p = n & ( for k being Element of NAT st k in n holds
p . k = H₁(k) ) ) from AFINSQ_1:sch 2();
then consider p being XFinSequence such that
A3: ( len p = n & ( for k being Element of NAT st k in n holds
p . k = H₁(k) ) ) ;
rng p c= D

proof

let y be set ; :: 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 set such that
A4: ( x in dom p & y = p . x ) by FUNCT_1:def 5;
reconsider nx = x as Ordinal by A4;
reconsider kx = nx as Element of NAT by A4;
A6: p . kx = H₁(kx) by A3, A4;

now

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 A6; :: thesis: verum

end;

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

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

now

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

case A9: x in len q ; :: thesis: p . x in D

then A10: H₁(x) = q . x by A8, Def6;
kx > 0 by A7;
then A11: 0 + 1 <= kx by NAT_1:13;
kx < len q by A9, NAT_1:45;
then kx in Seg (len q) by A11, FINSEQ_1:3;
then x in dom q by FINSEQ_1:def 3;
then A12: q . x in rng q by FUNCT_1:def 5;
rng q c= D by FINSEQ_1:def 4;
hence p . x in D by A6, A10, A12; :: thesis: verum

end;

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

then A14: H₁(x) = q . x by A8, Def6;
kx > 0 by A7;
then 0 + 1 <= kx by NAT_1:13;
then kx in Seg (len q) by A13, FINSEQ_1:3;
then x in dom q by FINSEQ_1:def 3;
then A15: q . x in rng q by FUNCT_1:def 5;
rng q c= D by FINSEQ_1:def 4;
hence p . x in D by A6, A14, A15; :: thesis: verum

end;

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

then H₁(x) = d by A8, Def6;
hence p . x in D by A6; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

then reconsider p = p as XFinSequence of by RELAT_1:def 19;
reconsider p2 = Replace p,0 ,d as XFinSequence of ;
A16: len p2 = len p by AFINSQ_1:48;
A17: p2 . 0 = len q by A1, A2, A3, AFINSQ_1:48;
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 A18: ( 1 <= i & i <= len q ) ; :: thesis: p2 . i = q . i
then i < n by A1, XXREAL_0:2;
then A19: i in n by NAT_1:45;
( i < len q or i = len q ) by A18, XXREAL_0:1;
then A20: ( i in len q or i = len q ) by NAT_1:45;
A21: i in NAT by ORDINAL1:def 13;
hence p2 . i = p . i by A18, AFINSQ_1:48
.= H₁(i) by A3, A19, A21
.= IFLGT i,(len q),(q . i),(q . i),d by A18, FUNCOP_1:def 8
.= q . i by A20, Def6 ;
:: thesis: verum

end;

then p2 is_an_xrep_of q by A1, A3, A16, A17, Def5;
hence ex p being XFinSequence of st
( len p = n & p is_an_xrep_of q ) by A3, A16; :: thesis: verum