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%> )
A1: rng F c= D by RELAT_1:def 19;
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
A2: F = G ^ <%x%> by AFINSQ_1:44;
len <%x%> = 1 by AFINSQ_1:36;
then A3: (len G) + 1 = len F by A2, AFINSQ_1:20;
A4: len G < (len G) + 1 by NAT_1:13;
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 y in rng G ; :: thesis: y in D
then consider x being set such that
A5: x in dom G and
A6: G . x = y by FUNCT_1:def 5;
dom G c= dom F by A3, A4, NAT_1:40;
then A7: F . x in rng F by A5, FUNCT_1:def 5;
A8: rng F c= D by RELAT_1:def 19;
F . x = G . x by A2, A5, AFINSQ_1:def 4;
hence y in D by A6, A7, A8; :: thesis: verum

end;

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