let b be non empty XFinSequence of REAL ; :: thesis: for a being Real
for m being Nat st b . 0 is Nat & len b = m & b . 0 < m holds
( ex c being XFinSequence of REAL st m scalar_prd_prg c,a,b & ( for c being non empty XFinSequence of REAL st m scalar_prd_prg c,a,b holds
XFS2FS* c = a * (XFS2FS* b) ) )
let a be 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 scalar_prd_prg c,a,b & ( for c being non empty XFinSequence of REAL st m scalar_prd_prg c,a,b holds
XFS2FS* c = a * (XFS2FS* b) ) )
let m be Nat; :: thesis: ( b . 0 is Nat & len b = m & b . 0 < m implies ( ex c being XFinSequence of REAL st m scalar_prd_prg c,a,b & ( for c being non empty XFinSequence of REAL st m scalar_prd_prg c,a,b holds
XFS2FS* c = a * (XFS2FS* b) ) ) )
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 scalar_prd_prg c,a,b & ( for c being non empty XFinSequence of REAL st m scalar_prd_prg c,a,b holds
XFS2FS* c = a * (XFS2FS* b) ) )
reconsider k = b . 0 as Nat by A1;
reconsider c2 = a * (XFS2FS* b) as FinSequence of REAL ;
dom (a * (XFS2FS* b)) = dom (XFS2FS* b) by VALUED_1:def 5;
then A4: Seg (len (a * (XFS2FS* b))) = dom (XFS2FS* b) by FINSEQ_1:def 3;
A5: b . 0 in Segm m by A1, A3, NAT_1:44;
then len (XFS2FS* b) = b . 0 by A2, AFINSQ_1:def 11;
then A6: len c2 = k by A4, FINSEQ_1:def 3;
then consider p being XFinSequence of REAL such that
A7: len p = m and
A8: p is_an_xrep_of c2 by A3, Th2, NUMBERS:19;
reconsider b0 = b . 0 as Element of REAL by XREAL_0:def 1;
reconsider p2 = Replace (p,0,b0) as XFinSequence of REAL ;

A9: now :: thesis: ( k <> 0 implies for i being Nat st 1 <= i & i <= k holds
p2 . i = a * (b . i) )

assume k <> 0 ; :: thesis: for i being Nat st 1 <= i & i <= k holds
p2 . i = a * (b . i)
thus for i being Nat st 1 <= i & i <= k holds
p2 . i = a * (b . i) :: thesis: verum

proof

let i be Nat; :: thesis: ( 1 <= i & i <= k implies p2 . i = a * (b . i) )
assume that
A10: 1 <= i and
A11: i <= k ; :: thesis: p2 . i = a * (b . i)
(XFS2FS* b) . i = b . i by A2, A5, A10, A11, AFINSQ_1:def 11;
then A12: (a * (XFS2FS* b)) . i = a * (b . i) by RVSUM_1:44;
( i in NAT & p . i = c2 . i ) by A6, A8, A10, A11, ORDINAL1:def 12;
hence p2 . i = a * (b . i) by A10, A12, AFINSQ_1:44; :: thesis: verum

end;

end;

( len p = len p2 & p2 . 0 = b . 0 ) by A1, A3, A7, AFINSQ_1:44;
then m scalar_prd_prg p2,a,b by A2, A7, A9;
hence ex c being XFinSequence of REAL st m scalar_prd_prg c,a,b ; :: thesis: for c being non empty XFinSequence of REAL st m scalar_prd_prg c,a,b holds
XFS2FS* c = a * (XFS2FS* b)
A13: 0 < len b ;
thus for c being non empty XFinSequence of REAL st m scalar_prd_prg c,a,b holds
XFS2FS* c = a * (XFS2FS* b) :: thesis: verum

proof

let c be non empty XFinSequence of REAL ; :: thesis: ( m scalar_prd_prg c,a,b implies XFS2FS* c = a * (XFS2FS* b) )
assume A14: m scalar_prd_prg c,a,b ; :: thesis: XFS2FS* c = a * (XFS2FS* b)
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 = a * (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 = a * (b . i) ) ) ) by A14;
then A19: len (XFS2FS* c) = c . 0 by A5, AFINSQ_1:def 11;

now :: thesis: ( ( n = 0 & XFS2FS* c = a * (XFS2FS* b) ) or ( n <> 0 & XFS2FS* c = a * (XFS2FS* b) ) )

per cases ( n = 0 or n <> 0 ) ;

case n = 0 ; :: thesis: XFS2FS* c = a * (XFS2FS* b)

then ( XFS2FS* b = <*> REAL & XFS2FS* c = <*> REAL ) by A13, A18, A16, AFINSQ_1:64;
hence XFS2FS* c = a * (XFS2FS* b) by RVSUM_1:46; :: thesis: verum

end;

case n <> 0 ; :: thesis: XFS2FS* c = a * (XFS2FS* b)

set p3 = XFS2FS* c;
for k3 being Nat st 1 <= k3 & k3 <= len (XFS2FS* c) holds
(XFS2FS* c) . k3 = c2 . k3

proof

let k3 be Nat; :: thesis: ( 1 <= k3 & k3 <= len (XFS2FS* c) implies (XFS2FS* c) . k3 = c2 . k3 )
assume that
A20: 1 <= k3 and
A21: k3 <= len (XFS2FS* c) ; :: thesis: (XFS2FS* c) . k3 = c2 . k3
A22: c . 0 in len c by A1, A3, A18, AFINSQ_1:86;
then A23: k3 <= n by A15, A16, A21, AFINSQ_1:def 11, A1;
then A24: b . k3 = (XFS2FS* b) . k3 by A2, A5, A16, A20, AFINSQ_1:def 11;
len (XFS2FS* c) = n by A15, A16, A22, AFINSQ_1:def 11, A1;
then (XFS2FS* c) . k3 = c . k3 by A15, A16, A20, A21, A22, AFINSQ_1:def 11
.= a * (b . k3) by A17, A20, A23 ;
hence (XFS2FS* c) . k3 = c2 . k3 by A24, RVSUM_1:44; :: thesis: verum

end;

hence XFS2FS* c = a * (XFS2FS* b) by A6, A15, A19, FINSEQ_1:14; :: thesis: verum

end;

end;

end;

hence XFS2FS* c = a * (XFS2FS* b) ; :: thesis: verum

end;