let b be non empty XFinSequence of REAL ; 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; 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; ( 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
; ( 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 ( k <> 0 implies for i being Nat st 1 <= i & i <= k holds
p2 . i = a * (b . i) )assume
k <> 0
;
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)
verumproof
let i be
Nat;
( 1 <= i & i <= k implies p2 . i = a * (b . i) )
assume that A10:
1
<= i
and A11:
i <= k
;
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;
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
; 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)
verumproof
let c be non
empty XFinSequence of
REAL ;
( m scalar_prd_prg c,a,b implies XFS2FS* c = a * (XFS2FS* b) )
assume A14:
m scalar_prd_prg c,
a,
b
;
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 ( ( 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
;
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;
( 1 <= k3 & k3 <= len (XFS2FS* c) implies (XFS2FS* c) . k3 = c2 . k3 )
assume that A20:
1
<= k3
and A21:
k3 <= len (XFS2FS* c)
;
(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;
verum
end; hence
XFS2FS* c = a * (XFS2FS* b)
by A6, A15, A19, FINSEQ_1:14;
verum end; end; end;
hence
XFS2FS* c = a * (XFS2FS* b)
;
verum
end;