let D be non empty set ; :: thesis: for F being XFinSequence of st F <> <%> D holds
ex G being XFinSequence of ex d being Element of D st F = G ^ <%d%>
let F be XFinSequence of ; :: thesis: ( F <> <%> D implies ex G being XFinSequence of ex d being Element of D st F = G ^ <%d%> )
assume F <> <%> D ; :: thesis: ex G being XFinSequence of ex d being Element of D st F = G ^ <%d%>
then consider G being XFinSequence, x being set such that
A1: F = G ^ <%x%> by AFINSQ_1:44;
len <%x%> = 1 by AFINSQ_1:36;
then A2: ( (len G) + 1 = len F & len G < (len G) + 1 & dom F = len F ) by A1, AFINSQ_1:20, NAT_1:13;
A3: rng G c= D

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng G or y in D )
assume A4: y in rng G ; :: thesis: y in D
consider x being set such that
A5: ( x in dom G & G . x = y ) by A4, FUNCT_1:def 5;
( dom G c= dom F & x is Element of NAT ) by A2, A5, NAT_1:40;
then ( F . x in rng F & rng F c= D & F . x = G . x ) by A1, A5, AFINSQ_1:def 4, FUNCT_1:def 5, RELAT_1:def 19;
hence y in D by A5; :: thesis: verum

end;

len G in dom F by A2, NAT_1:45;
then ( F . (len G) in rng F & rng F c= D ) by FUNCT_1:def 5, RELAT_1:def 19;
then ( G is XFinSequence of & x is Element of D ) by A1, A3, AFINSQ_1:40, RELAT_1:def 19;
hence ex G being XFinSequence of ex d being Element of D st F = G ^ <%d%> by A1; :: thesis: verum