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_{1}( 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_{1}(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_{1}(k)
;

rng p c= D

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

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

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

ex p being XFinSequence st

( len p = n & ( for k being Nat st k in n holds

p . k = H

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

rng p c= D

proof

then reconsider p = p as XFinSequence of D by RELAT_1:def 19;
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_{1}(kx)
by A5, A6, A7;

end;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

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

hence
y in D
by A8; :: thesis: verumper cases
( x = 0 or x <> 0 )
;

end;

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

then A11:
H_{1}(x) = IFLGT (x,(len q),(q . x),(q . x),d)
by FUNCOP_1:def 8;

end;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 ) )end;

hence
p . x in D
; :: thesis: verumper cases
( x in Segm (len q) or x = len q or ( not x in len q & not x = len q ) )
;

end;

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_{1}(x) = q . x
by A11, A12, Def2;

hence p . x in D by A9, A14, A15; :: thesis: verum

end;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

hence p . x in D by A9, A14, A15; :: thesis: verum

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_{1}(x) = q . x
by A11, A16, Def2;

hence p . x in D by A9, A17, A18; :: thesis: verum

end;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

hence p . x in D by A9, A17, A18; :: thesis: verum

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

A24:
len p2 = len p
by AFINSQ_1:44;
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_{1}(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;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

.= IFLGT (i,(len q),(q . i),(q . i),d) by A20, FUNCOP_1:def 8

.= q . i by A22, Def2 ;

:: thesis: verum

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