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 H1( 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 = H1(k) ) ) from then consider p being XFinSequence such that
A5: len p = n and
A6: for k being Nat st k in n holds
p . k = H1(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 = H1(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 A10: x <> 0 ; :: thesis: p . x in D
then A11: H1(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 ) ) ;
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 ;
then A22: ( i in Segm (len q) or i = len q ) by NAT_1:44;
i < n by ;
then A23: i in Segm n by NAT_1:44;
i in NAT by ORDINAL1:def 12;
hence p2 . i = p . i by
.= H1(i) by
.= IFLGT (i,(len q),(q . i),(q . i),d) by
.= q . i by ;
:: thesis: verum
end;
A24: len p2 = len p by AFINSQ_1:44;
p2 . 0 = len q by ;
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 ; :: thesis: verum