:: SEQ_1 semantic presentation

begin


definition
mode Real_Sequence is sequence of REAL;
end;


theorem Th1: :: SEQ_1:1
for f being Function holds
( f is Real_Sequence iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is real ) ) )
proof
let f be Function; ::_thesis: ( f is Real_Sequence iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is real ) ) )
thus  ( f is Real_Sequence implies ( dom f = NAT & ( for x being set st x in NAT holds
f . x is real ) ) ) by FUNCT_2:def_1; ::_thesis: ( dom f = NAT & ( for x being set st x in NAT holds
f . x is real ) implies f is Real_Sequence )
assume that
A1: dom f = NAT and
A2: for x being set st x in NAT holds
f . x is real ; ::_thesis: f is Real_Sequence
now__::_thesis:_for_y_being_set_st_y_in_rng_f_holds_
y_in_REAL
let y be set ; ::_thesis: ( y in rng f implies y in REAL )
assume  y in rng f ; ::_thesis: y in REAL
then consider x being set  such that
A3: x in dom f and
A4: y = f . x by FUNCT_1:def_3;
 f . x is real by A1, A2, A3;
hence  y in REAL by A4, XREAL_0:def_1; ::_thesis: verum
end;
then  rng f c= REAL by TARSKI:def_3;
hence  f is Real_Sequence by A1, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;

theorem Th2: :: SEQ_1:2
for f being Function holds
( f is Real_Sequence iff ( dom f = NAT & ( for n being Element of NAT holds f . n is real ) ) )
proof
let f be Function; ::_thesis: ( f is Real_Sequence iff ( dom f = NAT & ( for n being Element of NAT holds f . n is real ) ) )
thus  ( f is Real_Sequence implies ( dom f = NAT & ( for n being Element of NAT holds f . n is real ) ) ) by Th1; ::_thesis: ( dom f = NAT & ( for n being Element of NAT holds f . n is real ) implies f is Real_Sequence )
assume that
A1: dom f = NAT and
A2: for n being Element of NAT holds f . n is real ; ::_thesis: f is Real_Sequence
 for x being set st x in NAT holds
f . x is real by A2;
hence  f is Real_Sequence by A1, Th1; ::_thesis: verum
end;

definition
let f be real-valued Function;
let x be set ;
:: original: .
redefine funcf . x ->  Real;
coherence
 f . x is Real by XREAL_0:def_1;
end;

registration
cluster Relation-like non-zero NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued for Element of K19(K20(NAT,REAL));
existence
 ex b1 being PartFunc of NAT,REAL st b1 is non-zero
proof
reconsider p = NAT --> 1 as PartFunc of NAT,REAL by FUNCOP_1:46;
take  p ; ::_thesis: p is non-zero
 rng p = {1} by FUNCOP_1:8;
hence  not 0 in rng p by TARSKI:def_1; :: according to RELAT_1:def_9 ::_thesis: verum
end;
end;

theorem :: SEQ_1:3
for f being non-zero PartFunc of NAT,REAL holds rng f c= REAL \ {0}
proof
let f be non-zero PartFunc of NAT,REAL; ::_thesis: rng f c= REAL \ {0}
 not {} in rng f by RELAT_1:def_9;
hence  rng f c= REAL \ {0} by ZFMISC_1:34; ::_thesis: verum
end;

theorem Th4: :: SEQ_1:4
for seq being Real_Sequence holds
( seq is non-zero iff for x being set st x in NAT holds
seq . x <> 0 )
proof
let seq be Real_Sequence; ::_thesis: ( seq is non-zero iff for x being set st x in NAT holds
seq . x <> 0 )
thus  ( seq is non-zero implies for x being set st x in NAT holds
seq . x <> 0 ) ::_thesis: ( ( for x being set st x in NAT holds
seq . x <> 0 ) implies seq is non-zero )
proof
assume A1: seq is non-zero ; ::_thesis: for x being set st x in NAT holds
seq . x <> 0
let x be set ; ::_thesis: ( x in NAT implies seq . x <> 0 )
assume  x in NAT ; ::_thesis: seq . x <> 0
then  x in dom seq by Th2;
then  seq . x in rng seq by FUNCT_1:def_3;
hence  seq . x <> 0 by A1, RELAT_1:def_9; ::_thesis: verum
end;
assume A2: for x being set st x in NAT holds
seq . x <> 0 ; ::_thesis: seq is non-zero
assume  0 in rng seq ; :: according to RELAT_1:def_9 ::_thesis: contradiction
then  ex x being set st
( x in dom seq & seq . x = 0 ) by FUNCT_1:def_3;
hence  contradiction by A2; ::_thesis: verum
end;

theorem Th5: :: SEQ_1:5
for seq being Real_Sequence holds
( seq is non-zero iff for n being Element of NAT holds seq . n <> 0 )
proof
let seq be Real_Sequence; ::_thesis: ( seq is non-zero iff for n being Element of NAT holds seq . n <> 0 )
thus  ( seq is non-zero implies for n being Element of NAT holds seq . n <> 0 ) by Th4; ::_thesis: ( ( for n being Element of NAT holds seq . n <> 0 ) implies seq is non-zero )
assume  for n being Element of NAT holds seq . n <> 0 ; ::_thesis: seq is non-zero
then  for x being set st x in NAT holds
seq . x <> 0 ;
hence  seq is non-zero by Th4; ::_thesis: verum
end;

theorem :: SEQ_1:6
for r being real number ex seq being Real_Sequence st rng seq = {r}
proof
let r be real number ; ::_thesis: ex seq being Real_Sequence st rng seq = {r}
consider f being Function such that
A1: dom f = NAT and
A2: rng f = {r} by FUNCT_1:5;
 for x being set st x in {r} holds
x in REAL by XREAL_0:def_1;
then  rng f c= REAL by A2, TARSKI:def_3;
then reconsider f = f as Real_Sequence by A1, FUNCT_2:def_1, RELSET_1:4;
take  f ; ::_thesis: rng f = {r}
thus  rng f = {r} by A2; ::_thesis: verum
end;

scheme :: SEQ_1:sch 1
ExRealSeq{ F1( set ) ->  real number } :
 ex seq being Real_Sequence st
for n being Element of NAT holds seq . n = F1(n)
proof
defpred S1[ set , set ] means  ex n being Element of NAT st
( n = $1 & $2 = F1(n) );
A1: now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
ex_y_being_set_st_S1[x,y]
let x be set ; ::_thesis: ( x in NAT implies ex y being set st S1[x,y] )
assume  x in NAT ; ::_thesis: ex y being set st S1[x,y]
then consider n being Element of NAT  such that
A2: n = x ;
reconsider r2 = F1(n) as set ;
take y = r2; ::_thesis: S1[x,y]
thus  S1[x,y] by A2; ::_thesis: verum
end;
consider f being Function such that
A3: dom f = NAT and
A4: for x being set st x in NAT holds
S1[x,f . x] from CLASSES1:sch_1(A1);
now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
f_._x_is_real
let x be set ; ::_thesis: ( x in NAT implies f . x is real )
assume  x in NAT ; ::_thesis: f . x is real
then  ex n being Element of NAT st
( n = x & f . x = F1(n) ) by A4;
hence  f . x is real ; ::_thesis: verum
end;
then reconsider f = f as Real_Sequence by A3, Th1;
take seq = f; ::_thesis: for n being Element of NAT holds seq . n = F1(n)
let n be Element of NAT ; ::_thesis: seq . n = F1(n)
 ex k being Element of NAT st
( k = n & seq . n = F1(k) ) by A4;
hence  seq . n = F1(n) ; ::_thesis: verum
end;

scheme :: SEQ_1:sch 2
PartFuncExD9{ F1() ->  non empty set , F2() ->  non empty set , P1[ set , set ] } :
 ex f being PartFunc of F1(),F2() st
( ( for d being Element of F1() holds
( d in dom f iff ex c being Element of F2() st P1[d,c] ) ) & ( for d being Element of F1() st d in dom f holds
P1[d,f . d] ) )
proof
defpred S1[ set ] means  ex c being Element of F2() st P1[$1,c];
set x = the Element of F2();
defpred S2[ Element of F1(), Element of F2()] means ( ( ex c being Element of F2() st P1[$1,c] implies P1[$1,$2] ) & ( ( for c being Element of F2() holds P1[$1,c] ) implies $2 = the Element of F2() ) );
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in F1() & S1[x] ) ) from XBOOLE_0:sch_1();
 for x being set st x in X holds
x in F1() by A1;
then reconsider X = X as Subset of F1() by TARSKI:def_3;
A2: for d being Element of F1() ex z being Element of F2() st S2[d,z]
proof
let d be Element of F1(); ::_thesis: ex z being Element of F2() st S2[d,z]
 ( ( for c being Element of F2() holds P1[d,c] ) implies ex z being set st
( ( ex c being Element of F2() st P1[d,c] implies P1[d,z] ) & ( ( for c being Element of F2() holds P1[d,c] ) implies z = the Element of F2() ) ) ) ;
hence  ex z being Element of F2() st S2[d,z] ; ::_thesis: verum
end;
consider g being Function of F1(),F2() such that
A3: for d being Element of F1() holds S2[d,g . d] from FUNCT_2:sch_3(A2);
reconsider f = g | X as PartFunc of F1(),F2() ;
take  f ; ::_thesis: ( ( for d being Element of F1() holds
( d in dom f iff ex c being Element of F2() st P1[d,c] ) ) & ( for d being Element of F1() st d in dom f holds
P1[d,f . d] ) )
A4: dom g = F1() by FUNCT_2:def_1;
thus  for d being Element of F1() holds
( d in dom f iff ex c being Element of F2() st P1[d,c] ) ::_thesis: for d being Element of F1() st d in dom f holds
P1[d,f . d]
proof
let d be Element of F1(); ::_thesis: ( d in dom f iff ex c being Element of F2() st P1[d,c] )
 dom f c= X by RELAT_1:58;
hence  ( d in dom f implies ex c being Element of F2() st P1[d,c] ) by A1; ::_thesis: ( ex c being Element of F2() st P1[d,c] implies d in dom f )
assume  ex c being Element of F2() st P1[d,c] ; ::_thesis: d in dom f
then  d in X by A1;
then  d in (dom g) /\ X by A4, XBOOLE_0:def_4;
hence  d in dom f by RELAT_1:61; ::_thesis: verum
end;
let d be Element of F1(); ::_thesis: ( d in dom f implies P1[d,f . d] )
assume A5: d in dom f ; ::_thesis: P1[d,f . d]
 dom f c= X by RELAT_1:58;
then  ex c being Element of F2() st P1[d,c] by A1, A5;
then  P1[d,g . d] by A3;
hence  P1[d,f . d] by A5, FUNCT_1:47; ::_thesis: verum
end;

scheme :: SEQ_1:sch 3
LambdaPFD9{ F1() ->  non empty set , F2() ->  non empty set , F3( set ) ->  Element of F2(), P1[ set ] } :
 ex f being PartFunc of F1(),F2() st
( ( for d being Element of F1() holds
( d in dom f iff P1[d] ) ) & ( for d being Element of F1() st d in dom f holds
f . d = F3(d) ) )
proof
defpred S1[ Element of F1(), set ] means ( P1[$1] & $2 = F3($1) );
consider f being PartFunc of F1(),F2() such that
A1: for d being Element of F1() holds
( d in dom f iff ex c being Element of F2() st S1[d,c] ) and
A2: for d being Element of F1() st d in dom f holds
S1[d,f . d] from SEQ_1:sch_2();
take  f ; ::_thesis: ( ( for d being Element of F1() holds
( d in dom f iff P1[d] ) ) & ( for d being Element of F1() st d in dom f holds
f . d = F3(d) ) )
thus  for d being Element of F1() holds
( d in dom f iff P1[d] ) ::_thesis: for d being Element of F1() st d in dom f holds
f . d = F3(d)
proof
let d be Element of F1(); ::_thesis: ( d in dom f iff P1[d] )
thus  ( d in dom f implies P1[d] ) ::_thesis: ( P1[d] implies d in dom f )
proof
assume  d in dom f ; ::_thesis: P1[d]
then  ex c being Element of F2() st
( P1[d] & c = F3(d) ) by A1;
hence  P1[d] ; ::_thesis: verum
end;
assume  P1[d] ; ::_thesis: d in dom f
then  ex c being Element of F2() st
( P1[d] & c = F3(d) ) ;
hence  d in dom f by A1; ::_thesis: verum
end;
thus  for d being Element of F1() st d in dom f holds
f . d = F3(d) by A2; ::_thesis: verum
end;

scheme :: SEQ_1:sch 4
UnPartFuncD9{ F1() ->  set , F2() ->  set , F3() ->  set , F4( set ) ->  set } :
 for f, g being PartFunc of F1(),F2() st dom f = F3() & ( for c being Element of F1() st c in dom f holds
f . c = F4(c) ) & dom g = F3() & ( for c being Element of F1() st c in dom g holds
g . c = F4(c) ) holds
f = g
proof
let f, g be PartFunc of F1(),F2(); ::_thesis: ( dom f = F3() & ( for c being Element of F1() st c in dom f holds
f . c = F4(c) ) & dom g = F3() & ( for c being Element of F1() st c in dom g holds
g . c = F4(c) ) implies f = g )
assume that
A1: dom f = F3() and
A2: for c being Element of F1() st c in dom f holds
f . c = F4(c) and
A3: dom g = F3() and
A4: for c being Element of F1() st c in dom g holds
g . c = F4(c) ; ::_thesis: f = g
now__::_thesis:_for_c_being_Element_of_F1()_st_c_in_dom_f_holds_
f_._c_=_g_._c
let c be Element of F1(); ::_thesis: ( c in dom f implies f . c = g . c )
assume A5: c in dom f ; ::_thesis: f . c = g . c
hence f . c = F4(c) by A2
.= g . c by A1, A3, A4, A5 ;
::_thesis: verum
end;
hence  f = g by A1, A3, PARTFUN1:5; ::_thesis: verum
end;

theorem Th7: :: SEQ_1:7
for seq, seq1, seq2 being Real_Sequence holds
( seq = seq1 + seq2 iff for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) )
proof
let seq, seq1, seq2 be Real_Sequence; ::_thesis: ( seq = seq1 + seq2 iff for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) )
thus  ( seq = seq1 + seq2 implies for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ) ::_thesis: ( ( for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ) implies seq = seq1 + seq2 )
proof
assume A1: seq = seq1 + seq2 ; ::_thesis: for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n)
let n be Element of NAT ; ::_thesis: seq . n = (seq1 . n) + (seq2 . n)
 dom seq = NAT by FUNCT_2:def_1;
hence  seq . n = (seq1 . n) + (seq2 . n) by A1, VALUED_1:def_1; ::_thesis: verum
end;
assume  for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ; ::_thesis: seq = seq1 + seq2
then A2: for n being set st n in dom seq holds
seq . n = (seq1 . n) + (seq2 . n) ;
dom seq = NAT /\ NAT by FUNCT_2:def_1
.= NAT /\ (dom seq2) by FUNCT_2:def_1
.= (dom seq1) /\ (dom seq2) by FUNCT_2:def_1 ;
hence  seq = seq1 + seq2 by A2, VALUED_1:def_1; ::_thesis: verum
end;

theorem Th8: :: SEQ_1:8
for seq, seq1, seq2 being Real_Sequence holds
( seq = seq1 (#) seq2 iff for n being Element of NAT holds seq . n = (seq1 . n) * (seq2 . n) )
proof
let seq, seq1, seq2 be Real_Sequence; ::_thesis: ( seq = seq1 (#) seq2 iff for n being Element of NAT holds seq . n = (seq1 . n) * (seq2 . n) )
thus  ( seq = seq1 (#) seq2 implies for n being Element of NAT holds seq . n = (seq1 . n) * (seq2 . n) ) ::_thesis: ( ( for n being Element of NAT holds seq . n = (seq1 . n) * (seq2 . n) ) implies seq = seq1 (#) seq2 )
proof
assume A1: seq = seq1 (#) seq2 ; ::_thesis: for n being Element of NAT holds seq . n = (seq1 . n) * (seq2 . n)
let n be Element of NAT ; ::_thesis: seq . n = (seq1 . n) * (seq2 . n)
 dom seq = NAT by FUNCT_2:def_1;
hence  seq . n = (seq1 . n) * (seq2 . n) by A1, VALUED_1:def_4; ::_thesis: verum
end;
assume  for n being Element of NAT holds seq . n = (seq1 . n) * (seq2 . n) ; ::_thesis: seq = seq1 (#) seq2
then A2: for n being set st n in dom seq holds
seq . n = (seq1 . n) * (seq2 . n) ;
dom seq = NAT /\ NAT by FUNCT_2:def_1
.= NAT /\ (dom seq2) by FUNCT_2:def_1
.= (dom seq1) /\ (dom seq2) by FUNCT_2:def_1 ;
hence  seq = seq1 (#) seq2 by A2, VALUED_1:def_4; ::_thesis: verum
end;

theorem Th9: :: SEQ_1:9
for r being real number
for seq1, seq2 being Real_Sequence holds
( seq1 = r (#) seq2 iff for n being Element of NAT holds seq1 . n = r * (seq2 . n) )
proof
let r be real number ; ::_thesis: for seq1, seq2 being Real_Sequence holds
( seq1 = r (#) seq2 iff for n being Element of NAT holds seq1 . n = r * (seq2 . n) )
let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 = r (#) seq2 iff for n being Element of NAT holds seq1 . n = r * (seq2 . n) )
thus  ( seq1 = r (#) seq2 implies for n being Element of NAT holds seq1 . n = r * (seq2 . n) ) by VALUED_1:6; ::_thesis: ( ( for n being Element of NAT holds seq1 . n = r * (seq2 . n) ) implies seq1 = r (#) seq2 )
assume  for n being Element of NAT holds seq1 . n = r * (seq2 . n) ; ::_thesis: seq1 = r (#) seq2
then A1: for n being set st n in dom seq1 holds
seq1 . n = r * (seq2 . n) ;
dom seq1 = NAT by FUNCT_2:def_1
.= dom seq2 by FUNCT_2:def_1 ;
hence  seq1 = r (#) seq2 by A1, VALUED_1:def_5; ::_thesis: verum
end;

theorem :: SEQ_1:10
for seq1, seq2 being Real_Sequence holds
( seq1 = - seq2 iff for n being Element of NAT holds seq1 . n = - (seq2 . n) )
proof
let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 = - seq2 iff for n being Element of NAT holds seq1 . n = - (seq2 . n) )
thus  ( seq1 = - seq2 implies for n being Element of NAT holds seq1 . n = - (seq2 . n) ) by VALUED_1:8; ::_thesis: ( ( for n being Element of NAT holds seq1 . n = - (seq2 . n) ) implies seq1 = - seq2 )
assume  for n being Element of NAT holds seq1 . n = - (seq2 . n) ; ::_thesis: seq1 = - seq2
then A1: for n being set st n in dom seq1 holds
seq1 . n = - (seq2 . n) ;
dom seq1 = NAT by FUNCT_2:def_1
.= dom seq2 by FUNCT_2:def_1 ;
hence  seq1 = - seq2 by A1, VALUED_1:9; ::_thesis: verum
end;

theorem :: SEQ_1:11
for seq1, seq2 being Real_Sequence holds seq1 - seq2 = seq1 + (- seq2) ;

theorem Th12: :: SEQ_1:12
for seq1, seq being Real_Sequence holds
( seq1 = abs seq iff for n being Element of NAT holds seq1 . n = abs (seq . n) )
proof
let seq1, seq be Real_Sequence; ::_thesis: ( seq1 = abs seq iff for n being Element of NAT holds seq1 . n = abs (seq . n) )
thus  ( seq1 = abs seq implies for n being Element of NAT holds seq1 . n = abs (seq . n) ) by VALUED_1:18; ::_thesis: ( ( for n being Element of NAT holds seq1 . n = abs (seq . n) ) implies seq1 = abs seq )
assume  for n being Element of NAT holds seq1 . n = abs (seq . n) ; ::_thesis: seq1 = abs seq
then A1: for n being set st n in dom seq1 holds
seq1 . n = abs (seq . n) ;
dom seq1 = NAT by FUNCT_2:def_1
.= dom seq by FUNCT_2:def_1 ;
hence  seq1 = abs seq by A1, VALUED_1:def_11; ::_thesis: verum
end;

theorem Th13: :: SEQ_1:13
for seq1, seq2, seq3 being Real_Sequence holds (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3)
proof
let seq1, seq2, seq3 be Real_Sequence; ::_thesis: (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_+_seq2)_+_seq3)_._n_=_(seq1_+_(seq2_+_seq3))_._n
let n be Element of NAT ; ::_thesis: ((seq1 + seq2) + seq3) . n = (seq1 + (seq2 + seq3)) . n
thus ((seq1 + seq2) + seq3) . n = ((seq1 + seq2) . n) + (seq3 . n) by Th7
.= ((seq1 . n) + (seq2 . n)) + (seq3 . n) by Th7
.= (seq1 . n) + ((seq2 . n) + (seq3 . n))
.= (seq1 . n) + ((seq2 + seq3) . n) by Th7
.= (seq1 + (seq2 + seq3)) . n by Th7 ; ::_thesis: verum
end;
hence  (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th14: :: SEQ_1:14
for seq1, seq2, seq3 being Real_Sequence holds (seq1 (#) seq2) (#) seq3 = seq1 (#) (seq2 (#) seq3)
proof
let seq1, seq2, seq3 be Real_Sequence; ::_thesis: (seq1 (#) seq2) (#) seq3 = seq1 (#) (seq2 (#) seq3)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_(#)_seq2)_(#)_seq3)_._n_=_(seq1_(#)_(seq2_(#)_seq3))_._n
let n be Element of NAT ; ::_thesis: ((seq1 (#) seq2) (#) seq3) . n = (seq1 (#) (seq2 (#) seq3)) . n
thus ((seq1 (#) seq2) (#) seq3) . n = ((seq1 (#) seq2) . n) * (seq3 . n) by Th8
.= ((seq1 . n) * (seq2 . n)) * (seq3 . n) by Th8
.= (seq1 . n) * ((seq2 . n) * (seq3 . n))
.= (seq1 . n) * ((seq2 (#) seq3) . n) by Th8
.= (seq1 (#) (seq2 (#) seq3)) . n by Th8 ; ::_thesis: verum
end;
hence  (seq1 (#) seq2) (#) seq3 = seq1 (#) (seq2 (#) seq3) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th15: :: SEQ_1:15
for seq1, seq2, seq3 being Real_Sequence holds (seq1 + seq2) (#) seq3 = (seq1 (#) seq3) + (seq2 (#) seq3)
proof
let seq1, seq2, seq3 be Real_Sequence; ::_thesis: (seq1 + seq2) (#) seq3 = (seq1 (#) seq3) + (seq2 (#) seq3)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_+_seq2)_(#)_seq3)_._n_=_((seq1_(#)_seq3)_+_(seq2_(#)_seq3))_._n
let n be Element of NAT ; ::_thesis: ((seq1 + seq2) (#) seq3) . n = ((seq1 (#) seq3) + (seq2 (#) seq3)) . n
thus ((seq1 + seq2) (#) seq3) . n = ((seq1 + seq2) . n) * (seq3 . n) by Th8
.= ((seq1 . n) + (seq2 . n)) * (seq3 . n) by Th7
.= ((seq1 . n) * (seq3 . n)) + ((seq2 . n) * (seq3 . n))
.= ((seq1 (#) seq3) . n) + ((seq2 . n) * (seq3 . n)) by Th8
.= ((seq1 (#) seq3) . n) + ((seq2 (#) seq3) . n) by Th8
.= ((seq1 (#) seq3) + (seq2 (#) seq3)) . n by Th7 ; ::_thesis: verum
end;
hence  (seq1 + seq2) (#) seq3 = (seq1 (#) seq3) + (seq2 (#) seq3) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: SEQ_1:16
for seq3, seq1, seq2 being Real_Sequence holds seq3 (#) (seq1 + seq2) = (seq3 (#) seq1) + (seq3 (#) seq2) by Th15;

theorem :: SEQ_1:17
for seq being Real_Sequence holds - seq = (- 1) (#) seq ;

theorem Th18: :: SEQ_1:18
for r being real number
for seq1, seq2 being Real_Sequence holds r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2
proof
let r be real number ; ::_thesis: for seq1, seq2 being Real_Sequence holds r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2
let seq1, seq2 be Real_Sequence; ::_thesis: r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2
now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_(seq1_(#)_seq2))_._n_=_((r_(#)_seq1)_(#)_seq2)_._n
let n be Element of NAT ; ::_thesis: (r (#) (seq1 (#) seq2)) . n = ((r (#) seq1) (#) seq2) . n
thus (r (#) (seq1 (#) seq2)) . n = r * ((seq1 (#) seq2) . n) by Th9
.= r * ((seq1 . n) * (seq2 . n)) by Th8
.= (r * (seq1 . n)) * (seq2 . n)
.= ((r (#) seq1) . n) * (seq2 . n) by Th9
.= ((r (#) seq1) (#) seq2) . n by Th8 ; ::_thesis: verum
end;
hence  r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2 by FUNCT_2:63; ::_thesis: verum
end;

theorem Th19: :: SEQ_1:19
for r being real number
for seq1, seq2 being Real_Sequence holds r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2)
proof
let r be real number ; ::_thesis: for seq1, seq2 being Real_Sequence holds r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2)
let seq1, seq2 be Real_Sequence; ::_thesis: r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2)
now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_(seq1_(#)_seq2))_._n_=_(seq1_(#)_(r_(#)_seq2))_._n
let n be Element of NAT ; ::_thesis: (r (#) (seq1 (#) seq2)) . n = (seq1 (#) (r (#) seq2)) . n
thus (r (#) (seq1 (#) seq2)) . n = r * ((seq1 (#) seq2) . n) by Th9
.= r * ((seq1 . n) * (seq2 . n)) by Th8
.= (seq1 . n) * (r * (seq2 . n))
.= (seq1 . n) * ((r (#) seq2) . n) by Th9
.= (seq1 (#) (r (#) seq2)) . n by Th8 ; ::_thesis: verum
end;
hence  r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th20: :: SEQ_1:20
for seq1, seq2, seq3 being Real_Sequence holds (seq1 - seq2) (#) seq3 = (seq1 (#) seq3) - (seq2 (#) seq3)
proof
let seq1, seq2, seq3 be Real_Sequence; ::_thesis: (seq1 - seq2) (#) seq3 = (seq1 (#) seq3) - (seq2 (#) seq3)
thus (seq1 - seq2) (#) seq3 = (seq1 (#) seq3) + ((- seq2) (#) seq3) by Th15
.= (seq1 (#) seq3) - (seq2 (#) seq3) by Th18 ; ::_thesis: verum
end;

theorem :: SEQ_1:21
for seq3, seq1, seq2 being Real_Sequence holds (seq3 (#) seq1) - (seq3 (#) seq2) = seq3 (#) (seq1 - seq2) by Th20;

theorem Th22: :: SEQ_1:22
for r being real number
for seq1, seq2 being Real_Sequence holds r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2)
proof
let r be real number ; ::_thesis: for seq1, seq2 being Real_Sequence holds r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2)
let seq1, seq2 be Real_Sequence; ::_thesis: r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2)
now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_(seq1_+_seq2))_._n_=_((r_(#)_seq1)_+_(r_(#)_seq2))_._n
let n be Element of NAT ; ::_thesis: (r (#) (seq1 + seq2)) . n = ((r (#) seq1) + (r (#) seq2)) . n
thus (r (#) (seq1 + seq2)) . n = r * ((seq1 + seq2) . n) by Th9
.= r * ((seq1 . n) + (seq2 . n)) by Th7
.= (r * (seq1 . n)) + (r * (seq2 . n))
.= ((r (#) seq1) . n) + (r * (seq2 . n)) by Th9
.= ((r (#) seq1) . n) + ((r (#) seq2) . n) by Th9
.= ((r (#) seq1) + (r (#) seq2)) . n by Th7 ; ::_thesis: verum
end;
hence  r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th23: :: SEQ_1:23
for r, p being real number
for seq being Real_Sequence holds (r * p) (#) seq = r (#) (p (#) seq)
proof
let r, p be real number ; ::_thesis: for seq being Real_Sequence holds (r * p) (#) seq = r (#) (p (#) seq)
let seq be Real_Sequence; ::_thesis: (r * p) (#) seq = r (#) (p (#) seq)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((r_*_p)_(#)_seq)_._n_=_(r_(#)_(p_(#)_seq))_._n
let n be Element of NAT ; ::_thesis: ((r * p) (#) seq) . n = (r (#) (p (#) seq)) . n
thus ((r * p) (#) seq) . n = (r * p) * (seq . n) by Th9
.= r * (p * (seq . n))
.= r * ((p (#) seq) . n) by Th9
.= (r (#) (p (#) seq)) . n by Th9 ; ::_thesis: verum
end;
hence  (r * p) (#) seq = r (#) (p (#) seq) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th24: :: SEQ_1:24
for r being real number
for seq1, seq2 being Real_Sequence holds r (#) (seq1 - seq2) = (r (#) seq1) - (r (#) seq2)
proof
let r be real number ; ::_thesis: for seq1, seq2 being Real_Sequence holds r (#) (seq1 - seq2) = (r (#) seq1) - (r (#) seq2)
let seq1, seq2 be Real_Sequence; ::_thesis: r (#) (seq1 - seq2) = (r (#) seq1) - (r (#) seq2)
thus r (#) (seq1 - seq2) = (r (#) seq1) + (r (#) (- seq2)) by Th22
.= (r (#) seq1) + (((- 1) * r) (#) seq2) by Th23
.= (r (#) seq1) - (r (#) seq2) by Th23 ; ::_thesis: verum
end;

theorem :: SEQ_1:25
for r being real number
for seq1, seq being Real_Sequence holds r (#) (seq1 /" seq) = (r (#) seq1) /" seq
proof
let r be real number ; ::_thesis: for seq1, seq being Real_Sequence holds r (#) (seq1 /" seq) = (r (#) seq1) /" seq
let seq1, seq be Real_Sequence; ::_thesis: r (#) (seq1 /" seq) = (r (#) seq1) /" seq
thus r (#) (seq1 /" seq) = r (#) (seq1 (#) (seq "))
.= (r (#) seq1) /" seq by Th18 ; ::_thesis: verum
end;

theorem :: SEQ_1:26
for seq1, seq2, seq3 being Real_Sequence holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3
proof
let seq1, seq2, seq3 be Real_Sequence; ::_thesis: seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3
thus seq1 - (seq2 + seq3) = seq1 + ((- seq2) + ((- 1) (#) seq3)) by Th22
.= (seq1 - seq2) - seq3 by Th13 ; ::_thesis: verum
end;

theorem :: SEQ_1:27
for seq being Real_Sequence holds 1 (#) seq = seq
proof
let seq be Real_Sequence; ::_thesis: 1 (#) seq = seq
now__::_thesis:_for_n_being_Element_of_NAT_holds_(1_(#)_seq)_._n_=_seq_._n
let n be Element of NAT ; ::_thesis: (1 (#) seq) . n = seq . n
thus (1 (#) seq) . n = 1 * (seq . n) by Th9
.= seq . n ; ::_thesis: verum
end;
hence  1 (#) seq = seq by FUNCT_2:63; ::_thesis: verum
end;

theorem :: SEQ_1:28
canceled;

theorem :: SEQ_1:29
for seq1, seq2 being Real_Sequence holds seq1 - (- seq2) = seq1 + seq2 ;

theorem :: SEQ_1:30
for seq1, seq2, seq3 being Real_Sequence holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
proof
let seq1, seq2, seq3 be Real_Sequence; ::_thesis: seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
thus seq1 - (seq2 - seq3) = seq1 + ((- seq2) - (- seq3)) by Th24
.= (seq1 - seq2) + seq3 by Th13 ; ::_thesis: verum
end;

theorem :: SEQ_1:31
for seq1, seq2, seq3 being Real_Sequence holds seq1 + (seq2 - seq3) = (seq1 + seq2) - seq3
proof
let seq1, seq2, seq3 be Real_Sequence; ::_thesis: seq1 + (seq2 - seq3) = (seq1 + seq2) - seq3
thus seq1 + (seq2 - seq3) = (seq1 + seq2) + (- seq3) by Th13
.= (seq1 + seq2) - seq3 ; ::_thesis: verum
end;

theorem :: SEQ_1:32
for seq1, seq2 being Real_Sequence holds
( (- seq1) (#) seq2 = - (seq1 (#) seq2) & seq1 (#) (- seq2) = - (seq1 (#) seq2) ) by Th18;

theorem Th33: :: SEQ_1:33
for seq being Real_Sequence st seq is non-zero holds
seq " is non-zero
proof
let seq be Real_Sequence; ::_thesis: ( seq is non-zero implies seq " is non-zero )
assume that
A1: seq is non-zero and
A2: not seq " is non-zero ; ::_thesis: contradiction
consider n1 being Element of NAT  such that
A3: (seq ") . n1 = 0 by A2, Th5;
 (seq . n1) " = (seq ") . n1 by VALUED_1:10;
hence  contradiction by A1, A3, Th5, XCMPLX_1:202; ::_thesis: verum
end;

theorem :: SEQ_1:34
canceled;

theorem Th35: :: SEQ_1:35
for seq, seq1 being Real_Sequence holds
( ( seq is non-zero & seq1 is non-zero ) iff seq (#) seq1 is non-zero )
proof
let seq, seq1 be Real_Sequence; ::_thesis: ( ( seq is non-zero & seq1 is non-zero ) iff seq (#) seq1 is non-zero )
thus  ( seq is non-zero & seq1 is non-zero implies seq (#) seq1 is non-zero ) ::_thesis: ( seq (#) seq1 is non-zero implies ( seq is non-zero & seq1 is non-zero ) )
proof
assume A1: ( seq is non-zero & seq1 is non-zero ) ; ::_thesis: seq (#) seq1 is non-zero
now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq_(#)_seq1)_._n_<>_0
let n be Element of NAT ; ::_thesis: (seq (#) seq1) . n <> 0
A2: (seq (#) seq1) . n = (seq . n) * (seq1 . n) by Th8;
 ( seq . n <> 0 & seq1 . n <> 0 ) by A1, Th5;
hence  (seq (#) seq1) . n <> 0 by A2, XCMPLX_1:6; ::_thesis: verum
end;
hence  seq (#) seq1 is non-zero by Th5; ::_thesis: verum
end;
assume A3: seq (#) seq1 is non-zero ; ::_thesis: ( seq is non-zero & seq1 is non-zero )
now__::_thesis:_for_n_being_Element_of_NAT_holds_seq_._n_<>_0
let n be Element of NAT ; ::_thesis: seq . n <> 0
 (seq (#) seq1) . n = (seq . n) * (seq1 . n) by Th8;
hence  seq . n <> 0 by A3, Th5; ::_thesis: verum
end;
hence  seq is non-zero by Th5; ::_thesis: seq1 is non-zero
now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_<>_0
let n be Element of NAT ; ::_thesis: seq1 . n <> 0
 (seq (#) seq1) . n = (seq . n) * (seq1 . n) by Th8;
hence  seq1 . n <> 0 by A3, Th5; ::_thesis: verum
end;
hence  seq1 is non-zero by Th5; ::_thesis: verum
end;

theorem Th36: :: SEQ_1:36
for seq, seq1 being Real_Sequence holds (seq ") (#) (seq1 ") = (seq (#) seq1) "
proof
let seq, seq1 be Real_Sequence; ::_thesis: (seq ") (#) (seq1 ") = (seq (#) seq1) "
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_")_(#)_(seq1_"))_._n_=_((seq_(#)_seq1)_")_._n
let n be Element of NAT ; ::_thesis: ((seq ") (#) (seq1 ")) . n = ((seq (#) seq1) ") . n
thus ((seq ") (#) (seq1 ")) . n = ((seq ") . n) * ((seq1 ") . n) by Th8
.= ((seq ") . n) * ((seq1 . n) ") by VALUED_1:10
.= ((seq . n) ") * ((seq1 . n) ") by VALUED_1:10
.= ((seq . n) * (seq1 . n)) " by XCMPLX_1:204
.= ((seq (#) seq1) . n) " by Th8
.= ((seq (#) seq1) ") . n by VALUED_1:10 ; ::_thesis: verum
end;
hence  (seq ") (#) (seq1 ") = (seq (#) seq1) " by FUNCT_2:63; ::_thesis: verum
end;

theorem :: SEQ_1:37
for seq, seq1 being Real_Sequence st seq is non-zero holds
(seq1 /" seq) (#) seq = seq1
proof
let seq, seq1 be Real_Sequence; ::_thesis: ( seq is non-zero implies (seq1 /" seq) (#) seq = seq1 )
assume A1: seq is non-zero ; ::_thesis: (seq1 /" seq) (#) seq = seq1
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_/"_seq)_(#)_seq)_._n_=_seq1_._n
let n be Element of NAT ; ::_thesis: ((seq1 /" seq) (#) seq) . n = seq1 . n
A2: seq . n <> 0 by A1, Th5;
thus ((seq1 /" seq) (#) seq) . n = ((seq1 (#) (seq ")) . n) * (seq . n) by Th8
.= ((seq1 . n) * ((seq ") . n)) * (seq . n) by Th8
.= ((seq1 . n) * ((seq . n) ")) * (seq . n) by VALUED_1:10
.= (seq1 . n) * (((seq . n) ") * (seq . n))
.= (seq1 . n) * 1 by A2, XCMPLX_0:def_7
.= seq1 . n ; ::_thesis: verum
end;
hence  (seq1 /" seq) (#) seq = seq1 by FUNCT_2:63; ::_thesis: verum
end;

theorem :: SEQ_1:38
for seq9, seq, seq19, seq1 being Real_Sequence holds (seq9 /" seq) (#) (seq19 /" seq1) = (seq9 (#) seq19) /" (seq (#) seq1)
proof
let seq9, seq, seq19, seq1 be Real_Sequence; ::_thesis: (seq9 /" seq) (#) (seq19 /" seq1) = (seq9 (#) seq19) /" (seq (#) seq1)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq9_/"_seq)_(#)_(seq19_/"_seq1))_._n_=_((seq9_(#)_seq19)_/"_(seq_(#)_seq1))_._n
let n be Element of NAT ; ::_thesis: ((seq9 /" seq) (#) (seq19 /" seq1)) . n = ((seq9 (#) seq19) /" (seq (#) seq1)) . n
thus ((seq9 /" seq) (#) (seq19 /" seq1)) . n = ((seq9 (#) (seq ")) . n) * ((seq19 /" seq1) . n) by Th8
.= ((seq9 . n) * ((seq ") . n)) * ((seq19 (#) (seq1 ")) . n) by Th8
.= ((seq9 . n) * ((seq ") . n)) * ((seq19 . n) * ((seq1 ") . n)) by Th8
.= (seq9 . n) * ((seq19 . n) * (((seq ") . n) * ((seq1 ") . n)))
.= (seq9 . n) * ((seq19 . n) * (((seq ") (#) (seq1 ")) . n)) by Th8
.= ((seq9 . n) * (seq19 . n)) * (((seq ") (#) (seq1 ")) . n)
.= ((seq9 . n) * (seq19 . n)) * (((seq (#) seq1) ") . n) by Th36
.= ((seq9 (#) seq19) . n) * (((seq (#) seq1) ") . n) by Th8
.= ((seq9 (#) seq19) /" (seq (#) seq1)) . n by Th8 ; ::_thesis: verum
end;
hence  (seq9 /" seq) (#) (seq19 /" seq1) = (seq9 (#) seq19) /" (seq (#) seq1) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: SEQ_1:39
for seq, seq1 being Real_Sequence st seq is non-zero & seq1 is non-zero holds
seq /" seq1 is non-zero
proof
let seq, seq1 be Real_Sequence; ::_thesis: ( seq is non-zero & seq1 is non-zero implies seq /" seq1 is non-zero )
assume that
A1: seq is non-zero and
A2: seq1 is non-zero ; ::_thesis: seq /" seq1 is non-zero
 seq1 " is non-zero by A2, Th33;
hence  seq /" seq1 is non-zero by A1, Th35; ::_thesis: verum
end;

theorem Th40: :: SEQ_1:40
for seq, seq1 being Real_Sequence holds (seq /" seq1) " = seq1 /" seq
proof
let seq, seq1 be Real_Sequence; ::_thesis: (seq /" seq1) " = seq1 /" seq
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_/"_seq1)_")_._n_=_(seq1_/"_seq)_._n
let n be Element of NAT ; ::_thesis: ((seq /" seq1) ") . n = (seq1 /" seq) . n
thus ((seq /" seq1) ") . n = ((seq ") (#) ((seq1 ") ")) . n by Th36
.= (seq1 /" seq) . n ; ::_thesis: verum
end;
hence  (seq /" seq1) " = seq1 /" seq by FUNCT_2:63; ::_thesis: verum
end;

theorem :: SEQ_1:41
for seq2, seq1, seq being Real_Sequence holds seq2 (#) (seq1 /" seq) = (seq2 (#) seq1) /" seq
proof
let seq2, seq1, seq be Real_Sequence; ::_thesis: seq2 (#) (seq1 /" seq) = (seq2 (#) seq1) /" seq
thus seq2 (#) (seq1 /" seq) = seq2 (#) (seq1 (#) (seq "))
.= (seq2 (#) seq1) /" seq by Th14 ; ::_thesis: verum
end;

theorem :: SEQ_1:42
for seq2, seq, seq1 being Real_Sequence holds seq2 /" (seq /" seq1) = (seq2 (#) seq1) /" seq
proof
let seq2, seq, seq1 be Real_Sequence; ::_thesis: seq2 /" (seq /" seq1) = (seq2 (#) seq1) /" seq
thus seq2 /" (seq /" seq1) = seq2 (#) (seq1 /" seq) by Th40
.= seq2 (#) (seq1 (#) (seq "))
.= (seq2 (#) seq1) /" seq by Th14 ; ::_thesis: verum
end;

theorem Th43: :: SEQ_1:43
for seq1, seq2, seq being Real_Sequence st seq1 is non-zero holds
seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1)
proof
let seq1, seq2, seq be Real_Sequence; ::_thesis: ( seq1 is non-zero implies seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1) )
assume A1: seq1 is non-zero ; ::_thesis: seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1)
now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq2_/"_seq)_._n_=_((seq2_(#)_seq1)_/"_(seq_(#)_seq1))_._n
let n be Element of NAT ; ::_thesis: (seq2 /" seq) . n = ((seq2 (#) seq1) /" (seq (#) seq1)) . n
A2: seq1 . n <> 0 by A1, Th5;
thus (seq2 /" seq) . n = ((seq2 . n) * 1) * ((seq ") . n) by Th8
.= ((seq2 . n) * ((seq1 . n) * ((seq1 . n) "))) * ((seq ") . n) by A2, XCMPLX_0:def_7
.= ((seq2 . n) * (seq1 . n)) * (((seq1 . n) ") * ((seq ") . n))
.= ((seq2 (#) seq1) . n) * (((seq1 . n) ") * ((seq ") . n)) by Th8
.= ((seq2 (#) seq1) . n) * (((seq1 ") . n) * ((seq ") . n)) by VALUED_1:10
.= ((seq2 (#) seq1) . n) * (((seq ") (#) (seq1 ")) . n) by Th8
.= ((seq2 (#) seq1) . n) * (((seq (#) seq1) ") . n) by Th36
.= ((seq2 (#) seq1) /" (seq (#) seq1)) . n by Th8 ; ::_thesis: verum
end;
hence  seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th44: :: SEQ_1:44
for r being real number
for seq being Real_Sequence st r <> 0 & seq is non-zero holds
r (#) seq is non-zero
proof
let r be real number ; ::_thesis: for seq being Real_Sequence st r <> 0 & seq is non-zero holds
r (#) seq is non-zero
let seq be Real_Sequence; ::_thesis: ( r <> 0 & seq is non-zero implies r (#) seq is non-zero )
assume that
A1: r <> 0 and
A2: seq is non-zero and
A3: not r (#) seq is non-zero ; ::_thesis: contradiction
consider n1 being Element of NAT  such that
A4: (r (#) seq) . n1 = 0 by A3, Th5;
A5: seq . n1 <> 0 by A2, Th5;
 r * (seq . n1) = 0 by A4, Th9;
hence  contradiction by A1, A5, XCMPLX_1:6; ::_thesis: verum
end;

theorem :: SEQ_1:45
for seq being Real_Sequence st seq is non-zero holds
- seq is non-zero by Th44;

theorem Th46: :: SEQ_1:46
for r being real number
for seq being Real_Sequence holds (r (#) seq) " = (r ") (#) (seq ")
proof
let r be real number ; ::_thesis: for seq being Real_Sequence holds (r (#) seq) " = (r ") (#) (seq ")
let seq be Real_Sequence; ::_thesis: (r (#) seq) " = (r ") (#) (seq ")
now__::_thesis:_for_n_being_Element_of_NAT_holds_((r_(#)_seq)_")_._n_=_((r_")_(#)_(seq_"))_._n
let n be Element of NAT ; ::_thesis: ((r (#) seq) ") . n = ((r ") (#) (seq ")) . n
thus ((r (#) seq) ") . n = ((r (#) seq) . n) " by VALUED_1:10
.= (r * (seq . n)) " by Th9
.= (r ") * ((seq . n) ") by XCMPLX_1:204
.= (r ") * ((seq ") . n) by VALUED_1:10
.= ((r ") (#) (seq ")) . n by Th9 ; ::_thesis: verum
end;
hence  (r (#) seq) " = (r ") (#) (seq ") by FUNCT_2:63; ::_thesis: verum
end;

Lm1:  (- 1) " = - 1
;

theorem :: SEQ_1:47
for seq being Real_Sequence holds (- seq) " = (- 1) (#) (seq ") by Lm1, Th46;

theorem :: SEQ_1:48
for seq1, seq being Real_Sequence holds
( - (seq1 /" seq) = (- seq1) /" seq & seq1 /" (- seq) = - (seq1 /" seq) )
proof
let seq1, seq be Real_Sequence; ::_thesis: ( - (seq1 /" seq) = (- seq1) /" seq & seq1 /" (- seq) = - (seq1 /" seq) )
thus  - (seq1 /" seq) = (- 1) (#) (seq1 (#) (seq "))
.= (- seq1) /" seq by Th18 ; ::_thesis: seq1 /" (- seq) = - (seq1 /" seq)
thus seq1 /" (- seq) = seq1 (#) ((- 1) (#) (seq ")) by Lm1, Th46
.= - (seq1 /" seq) by Th19 ; ::_thesis: verum
end;

theorem :: SEQ_1:49
for seq1, seq, seq19 being Real_Sequence holds
( (seq1 /" seq) + (seq19 /" seq) = (seq1 + seq19) /" seq & (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) /" seq )
proof
let seq1, seq, seq19 be Real_Sequence; ::_thesis: ( (seq1 /" seq) + (seq19 /" seq) = (seq1 + seq19) /" seq & (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) /" seq )
thus (seq1 /" seq) + (seq19 /" seq) = (seq1 + seq19) (#) (seq ") by Th15
.= (seq1 + seq19) /" seq ; ::_thesis: (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) /" seq
thus (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) (#) (seq ") by Th20
.= (seq1 - seq19) /" seq ; ::_thesis: verum
end;

theorem :: SEQ_1:50
for seq, seq9, seq1, seq19 being Real_Sequence st seq is non-zero & seq9 is non-zero holds
( (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) & (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) )
proof
let seq, seq9, seq1, seq19 be Real_Sequence; ::_thesis: ( seq is non-zero & seq9 is non-zero implies ( (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) & (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) ) )
assume that
A1: seq is non-zero and
A2: seq9 is non-zero ; ::_thesis: ( (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) & (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) )
thus (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) /" (seq (#) seq9)) + (seq19 /" seq9) by A2, Th43
.= ((seq1 (#) seq9) /" (seq (#) seq9)) + ((seq19 (#) seq) /" (seq (#) seq9)) by A1, Th43
.= ((seq1 (#) seq9) + (seq19 (#) seq)) (#) ((seq (#) seq9) ") by Th15
.= ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) ; ::_thesis: (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9)
thus (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) /" (seq (#) seq9)) - (seq19 /" seq9) by A2, Th43
.= ((seq1 (#) seq9) /" (seq (#) seq9)) - ((seq19 (#) seq) /" (seq (#) seq9)) by A1, Th43
.= ((seq1 (#) seq9) - (seq19 (#) seq)) (#) ((seq (#) seq9) ") by Th20
.= ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) ; ::_thesis: verum
end;

theorem :: SEQ_1:51
for seq19, seq, seq9, seq1 being Real_Sequence holds (seq19 /" seq) /" (seq9 /" seq1) = (seq19 (#) seq1) /" (seq (#) seq9)
proof
let seq19, seq, seq9, seq1 be Real_Sequence; ::_thesis: (seq19 /" seq) /" (seq9 /" seq1) = (seq19 (#) seq1) /" (seq (#) seq9)
thus (seq19 /" seq) /" (seq9 /" seq1) = (seq19 /" seq) (#) ((seq9 ") (#) ((seq1 ") ")) by Th36
.= ((seq19 (#) (seq ")) (#) seq1) (#) (seq9 ") by Th14
.= (seq19 (#) (seq1 (#) (seq "))) (#) (seq9 ") by Th14
.= seq19 (#) ((seq1 (#) (seq ")) (#) (seq9 ")) by Th14
.= seq19 (#) (seq1 (#) ((seq ") (#) (seq9 "))) by Th14
.= (seq19 (#) seq1) (#) ((seq ") (#) (seq9 ")) by Th14
.= (seq19 (#) seq1) /" (seq (#) seq9) by Th36 ; ::_thesis: verum
end;

theorem Th52: :: SEQ_1:52
for seq, seq9 being Real_Sequence holds abs (seq (#) seq9) = (abs seq) (#) (abs seq9)
proof
let seq, seq9 be Real_Sequence; ::_thesis: abs (seq (#) seq9) = (abs seq) (#) (abs seq9)
now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(seq_(#)_seq9))_._n_=_((abs_seq)_(#)_(abs_seq9))_._n
let n be Element of NAT ; ::_thesis: (abs (seq (#) seq9)) . n = ((abs seq) (#) (abs seq9)) . n
thus (abs (seq (#) seq9)) . n = abs ((seq (#) seq9) . n) by Th12
.= abs ((seq . n) * (seq9 . n)) by Th8
.= (abs (seq . n)) * (abs (seq9 . n)) by COMPLEX1:65
.= ((abs seq) . n) * (abs (seq9 . n)) by Th12
.= ((abs seq) . n) * ((abs seq9) . n) by Th12
.= ((abs seq) (#) (abs seq9)) . n by Th8 ; ::_thesis: verum
end;
hence  abs (seq (#) seq9) = (abs seq) (#) (abs seq9) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: SEQ_1:53
for seq being Real_Sequence st seq is non-zero holds
abs seq is non-zero
proof
let seq be Real_Sequence; ::_thesis: ( seq is non-zero implies abs seq is non-zero )
assume A1: seq is non-zero ; ::_thesis: abs seq is non-zero
now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_seq)_._n_<>_0
let n be Element of NAT ; ::_thesis: (abs seq) . n <> 0
 seq . n <> 0 by A1, Th5;
then  abs (seq . n) <> 0 by COMPLEX1:47;
hence  (abs seq) . n <> 0 by Th12; ::_thesis: verum
end;
hence  abs seq is non-zero by Th5; ::_thesis: verum
end;

theorem Th54: :: SEQ_1:54
for seq being Real_Sequence holds (abs seq) " = abs (seq ")
proof
let seq be Real_Sequence; ::_thesis: (abs seq) " = abs (seq ")
now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(seq_"))_._n_=_((abs_seq)_")_._n
let n be Element of NAT ; ::_thesis: (abs (seq ")) . n = ((abs seq) ") . n
thus (abs (seq ")) . n = abs ((seq ") . n) by Th12
.= abs ((seq . n) ") by VALUED_1:10
.= abs (1 / (seq . n)) by XCMPLX_1:215
.= 1 / (abs (seq . n)) by ABSVALUE:7
.= (abs (seq . n)) " by XCMPLX_1:215
.= ((abs seq) . n) " by Th12
.= ((abs seq) ") . n by VALUED_1:10 ; ::_thesis: verum
end;
hence  (abs seq) " = abs (seq ") by FUNCT_2:63; ::_thesis: verum
end;

theorem :: SEQ_1:55
for seq9, seq being Real_Sequence holds abs (seq9 /" seq) = (abs seq9) /" (abs seq)
proof
let seq9, seq be Real_Sequence; ::_thesis: abs (seq9 /" seq) = (abs seq9) /" (abs seq)
thus  abs (seq9 /" seq) = (abs seq9) (#) (abs (seq ")) by Th52
.= (abs seq9) /" (abs seq) by Th54 ; ::_thesis: verum
end;

theorem :: SEQ_1:56
for r being real number
for seq being Real_Sequence holds abs (r (#) seq) = (abs r) (#) (abs seq)
proof
let r be real number ; ::_thesis: for seq being Real_Sequence holds abs (r (#) seq) = (abs r) (#) (abs seq)
let seq be Real_Sequence; ::_thesis: abs (r (#) seq) = (abs r) (#) (abs seq)
now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(r_(#)_seq))_._n_=_((abs_r)_(#)_(abs_seq))_._n
let n be Element of NAT ; ::_thesis: (abs (r (#) seq)) . n = ((abs r) (#) (abs seq)) . n
thus (abs (r (#) seq)) . n = abs ((r (#) seq) . n) by Th12
.= abs (r * (seq . n)) by Th9
.= (abs r) * (abs (seq . n)) by COMPLEX1:65
.= (abs r) * ((abs seq) . n) by Th12
.= ((abs r) (#) (abs seq)) . n by Th9 ; ::_thesis: verum
end;
hence  abs (r (#) seq) = (abs r) (#) (abs seq) by FUNCT_2:63; ::_thesis: verum
end;