let b be non empty XFinSequence of REAL ; :: thesis: for m being Nat st b . 0 is Nat & len b = m & b . 0 < m holds
( ex c being XFinSequence of REAL st m vector_minus_prg c,b & ( for c being non empty XFinSequence of REAL st m vector_minus_prg c,b holds
XFS2FS* c = - () ) )

let m be Nat; :: thesis: ( b . 0 is Nat & len b = m & b . 0 < m implies ( ex c being XFinSequence of REAL st m vector_minus_prg c,b & ( for c being non empty XFinSequence of REAL st m vector_minus_prg c,b holds
XFS2FS* c = - () ) ) )

assume that
A1: b . 0 is Nat and
A2: len b = m and
A3: b . 0 < m ; :: thesis: ( ex c being XFinSequence of REAL st m vector_minus_prg c,b & ( for c being non empty XFinSequence of REAL st m vector_minus_prg c,b holds
XFS2FS* c = - () ) )

reconsider k = b . 0 as Nat by A1;
reconsider c2 = - () as FinSequence of REAL ;
dom (- ()) = dom () by VALUED_1:8;
then A4: Seg (len (- ())) = dom () by FINSEQ_1:def 3;
A5: b . 0 in Segm m by ;
then len () = b . 0 by ;
then A6: len c2 = k by ;
then consider p being XFinSequence of REAL such that
A7: len p = m and
A8: p is_an_xrep_of c2 by ;
reconsider b0 = b . 0 as Element of REAL by XREAL_0:def 1;
reconsider p2 = Replace (p,0,b0) as XFinSequence of REAL ;
A9: ( k <> 0 implies for i being Nat st 1 <= i & i <= k holds
p2 . i = - (b . i) )
proof
assume k <> 0 ; :: thesis: for i being Nat st 1 <= i & i <= k holds
p2 . i = - (b . i)

let i be Nat; :: thesis: ( 1 <= i & i <= k implies p2 . i = - (b . i) )
assume that
A10: 1 <= i and
A11: i <= k ; :: thesis: p2 . i = - (b . i)
(XFS2FS* b) . i = b . i by ;
then A12: (- ()) . i = - (b . i) by RVSUM_1:17;
( i in NAT & p . i = c2 . i ) by ;
hence p2 . i = - (b . i) by ; :: thesis: verum
end;
( len p = len p2 & p2 . 0 = b . 0 ) by ;
then m vector_minus_prg p2,b by A2, A7, A9;
hence ex c being XFinSequence of REAL st m vector_minus_prg c,b ; :: thesis: for c being non empty XFinSequence of REAL st m vector_minus_prg c,b holds
XFS2FS* c = - ()

A13: 0 < len b ;
thus for c being non empty XFinSequence of REAL st m vector_minus_prg c,b holds
XFS2FS* c = - () :: thesis: verum
proof
let c be non empty XFinSequence of REAL ; :: thesis: ( m vector_minus_prg c,b implies XFS2FS* c = - () )
assume A14: m vector_minus_prg c,b ; :: thesis: XFS2FS* c = - ()
then consider n being Integer such that
A15: c . 0 = b . 0 and
A16: n = b . 0 and
A17: ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
c . i = - (b . i) ) ;
A18: ( len c = m & ex n being Integer st
( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
c . i = - (b . i) ) ) ) by A14;
then A19: len () = c . 0 by ;
now :: thesis: ( ( n = 0 & XFS2FS* c = - () ) or ( n <> 0 & XFS2FS* c = - () ) )
per cases ( n = 0 or n <> 0 ) ;
case n <> 0 ; :: thesis: XFS2FS* c = - ()
set p3 = XFS2FS* c;
for k3 being Nat st 1 <= k3 & k3 <= len () holds
() . k3 = c2 . k3
proof
let k3 be Nat; :: thesis: ( 1 <= k3 & k3 <= len () implies () . k3 = c2 . k3 )
A21: c . 0 in len c by ;
then A22: len () = n by ;
assume A23: ( 1 <= k3 & k3 <= len () ) ; :: thesis: () . k3 = c2 . k3
then A24: b . k3 = () . k3 by ;
() . k3 = c . k3 by
.= - (b . k3) by ;
hence (XFS2FS* c) . k3 = c2 . k3 by ; :: thesis: verum
end;
hence XFS2FS* c = - () by ; :: thesis: verum
end;
end;
end;
hence XFS2FS* c = - () ; :: thesis: verum
end;