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

proof

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

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

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

take F . x ; :: thesis: ( F . x in COMPLEX & S₁[x,F . x] )
F . x in COMPLEX by XCMPLX_0:def 2;
hence ( F . x in COMPLEX & S₁[x,F . x] ) by A2; :: thesis: verum

end;

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

take 0 ; :: thesis: ( 0 in COMPLEX & S₁[x, 0 ] )
0 in COMPLEX by XCMPLX_0:def 2;
hence ( 0 in COMPLEX & S₁[x, 0 ] ) by A3; :: thesis: verum

end;

end;

end;

ex G1 being sequence of COMPLEX st
for x being object st x in NAT holds
S₁[x,G1 . x] from FUNCT_2:sch 1(A1);
then consider G2 being sequence of COMPLEX such that
A4: for x being object 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 that
A5: 1 <= n and
A6: n <= len F ; :: thesis: G2 . n = F . n
n in Seg (len F) by A5, A6, FINSEQ_1:1;
hence G2 . n = F . n by A4; :: thesis: verum

end;

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