let b be non empty XFinSequence of ; :: thesis: for a being Real
for m being Nat st b . 0 is Nat & len b = m & 0 <= b . 0 & b . 0 < m holds
( ex c being XFinSequence of st m scalar_prd_prg c,a,b & ( for c being non empty XFinSequence of 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 & 0 <= b . 0 & b . 0 < m holds
( ex c being XFinSequence of st m scalar_prd_prg c,a,b & ( for c being non empty XFinSequence of 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 & 0 <= b . 0 & b . 0 < m implies ( ex c being XFinSequence of st m scalar_prd_prg c,a,b & ( for c being non empty XFinSequence of st m scalar_prd_prg c,a,b holds
XFS2FS* c = a * (XFS2FS* b) ) ) )
assume A1: ( b . 0 is Nat & len b = m & 0 <= b . 0 & b . 0 < m ) ; :: thesis: ( ex c being XFinSequence of st m scalar_prd_prg c,a,b & ( for c being non empty XFinSequence of st m scalar_prd_prg c,a,b holds
XFS2FS* c = a * (XFS2FS* b) ) )
then A2: b . 0 in m by NAT_1:45;
A3: 0 < len b by Th2;
reconsider k = b . 0 as Nat by A1;
reconsider c2 = a * (XFS2FS* b) as FinSequence of REAL ;
A4: len (XFS2FS* b) = b . 0 by A1, A2, Def4;
dom (a * (XFS2FS* b)) = dom (XFS2FS* b) by VALUED_1:def 5;
then Seg (len (a * (XFS2FS* b))) = dom (XFS2FS* b) by FINSEQ_1:def 3;
then A5: len c2 = k by A4, FINSEQ_1:def 3;
then consider p being XFinSequence of such that
A6: ( len p = m & p is_an_xrep_of c2 ) by A1, Th7;
set p2 = Replace p,0 ,(b . 0 );
A7: len p = len (Replace p,0 ,(b . 0 )) by AFINSQ_1:48;
ex n being Integer st
( (Replace p,0 ,(b . 0 )) . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
(Replace p,0 ,(b . 0 )) . i = a * (b . i) ) )

proof

A8: ( k <> 0 implies for i being Nat st 1 <= i & i <= k holds
(Replace p,0 ,(b . 0 )) . i = a * (b . i) )

proof

now

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

proof

let i be Nat; :: thesis: ( 1 <= i & i <= k implies (Replace p,0 ,(b . 0 )) . i = a * (b . i) )
A9: i in NAT by ORDINAL1:def 13;
assume A10: ( 1 <= i & i <= k ) ; :: thesis: (Replace p,0 ,(b . 0 )) . i = a * (b . i)
then A11: p . i = c2 . i by A5, A6, Def5;
(XFS2FS* b) . i = b . i by A1, A2, A10, Def4;
then (a * (XFS2FS* b)) . i = a * (b . i) by RVSUM_1:66;
hence (Replace p,0 ,(b . 0 )) . i = a * (b . i) by A9, A10, A11, AFINSQ_1:48; :: thesis: verum

end;

end;

hence ( k <> 0 implies for i being Nat st 1 <= i & i <= k holds
(Replace p,0 ,(b . 0 )) . i = a * (b . i) ) ; :: thesis: verum

end;

(Replace p,0 ,(b . 0 )) . 0 = b . 0 by A1, A6, AFINSQ_1:48;
hence ex n being Integer st
( (Replace p,0 ,(b . 0 )) . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
(Replace p,0 ,(b . 0 )) . i = a * (b . i) ) ) by A8; :: thesis: verum

end;

then m scalar_prd_prg Replace p,0 ,(b . 0 ),a,b by A1, A6, A7, Def8;
hence ex c being XFinSequence of st m scalar_prd_prg c,a,b ; :: thesis: for c being non empty XFinSequence of st m scalar_prd_prg c,a,b holds
XFS2FS* c = a * (XFS2FS* b)
thus for c being non empty XFinSequence of st m scalar_prd_prg c,a,b holds
XFS2FS* c = a * (XFS2FS* b) :: thesis: verum

proof

let c be non empty XFinSequence of ; :: thesis: ( m scalar_prd_prg c,a,b implies XFS2FS* c = a * (XFS2FS* b) )
assume A12: m scalar_prd_prg c,a,b ; :: thesis: XFS2FS* c = a * (XFS2FS* b)
then A13: ( len c = m & len b = 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 Def8;
consider n being Integer such that
A14: ( 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 A12, Def8;
A15: len (XFS2FS* c) = c . 0 by A2, A13, Def4;

now

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

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

then A17: XFS2FS* b = <*> REAL by A3, A14, Th5;
XFS2FS* c = <*> REAL by A3, A13, A14, A16, Th5;
hence XFS2FS* c = a * (XFS2FS* b) by A17, RVSUM_1:68; :: 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 A18: ( 1 <= k3 & k3 <= len (XFS2FS* c) ) ; :: thesis: (XFS2FS* c) . k3 = c2 . k3
A19: c . 0 in len c by A1, A13, NAT_1:45;
then A20: ( len (XFS2FS* c) = n & ( for i being Nat st 1 <= i & i <= n holds
(XFS2FS* c) . i = c . i ) ) by A14, Def4;
A21: ( 1 <= k3 & k3 <= n ) by A14, A18, A19, Def4;
A22: (XFS2FS* c) . k3 = c . k3 by A18, A20
.= a * (b . k3) by A14, A21 ;
b . k3 = (XFS2FS* b) . k3 by A1, A2, A14, A21, Def4;
hence (XFS2FS* c) . k3 = c2 . k3 by A22, RVSUM_1:66; :: thesis: verum

end;

hence XFS2FS* c = a * (XFS2FS* b) by A5, A14, A15, FINSEQ_1:18; :: thesis: verum

end;

end;

end;

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

end;