let F be FinSequence of COMPLEX ; :: thesis: ex G being Function of NAT ,COMPLEX st
for n being Nat st 1 <= n & n <= len F holds
G . n = F . n
defpred S₁[ set , set ] means ( ( $1 in Seg (len F) implies $2 = F . $1 ) & ( not $1 in Seg (len F) implies $2 = 0 ) );
A1: for x being set st x in NAT holds
ex y being set st
( y in COMPLEX & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in NAT implies ex y being set st
( y in COMPLEX & S₁[x,y] ) )
assume x in NAT ; :: thesis: ex y being set st
( y in COMPLEX & S₁[x,y] )

per cases ( x in Seg (len F) or not x in Seg (len F) ) ;

suppose x in Seg (len F) ; :: thesis: ex y being set st
( y in COMPLEX & S₁[x,y] )

hence ex y being set st
( y in COMPLEX & S₁[x,y] ) ; :: thesis: verum

end;

suppose not x in Seg (len F) ; :: thesis: ex y being set st
( y in COMPLEX & S₁[x,y] )

then not x in dom F by FINSEQ_1:def 3;
then S₁[x,F . x] by FUNCT_1:def 4;
hence ex y being set st
( y in COMPLEX & S₁[x,y] ) ; :: thesis: verum

end;

end;

end;

ex G1 being Function of NAT ,COMPLEX st
for x being set st x in NAT holds
S₁[x,G1 . x] from FUNCT_2:sch 1(A1);
then consider G2 being Function of NAT ,COMPLEX such that
A2: for x being set st x in NAT holds
( ( x in Seg (len F) implies G2 . x = F . x ) & ( not x in Seg (len F) implies G2 . x = 0 ) ) ;
for n being Nat st 1 <= n & n <= len F holds
G2 . n = F . n

proof

let n be Nat; :: thesis: ( 1 <= n & n <= len F implies G2 . n = F . n )
assume ( 1 <= n & n <= len F ) ; :: thesis: G2 . n = F . n
then n in Seg (len F) by FINSEQ_1:3;
hence G2 . n = F . n by A2; :: thesis: verum

end;

hence ex G being Function of NAT ,COMPLEX st
for n being Nat st 1 <= n & n <= len F holds
G . n = F . n ; :: thesis: verum