:: PRGCOR_2 semantic presentation

begin


definition
let D be non empty set ;
let p be XFinSequence of ;
let q be FinSequence of D;
predp is_an_xrep_of q means :Def1: :: PRGCOR_2:def 1
( NAT c= D & p . 0 = len q & len q < len p & ( for i being Nat st 1 <= i & i <= len q holds
p . i = q . i ) );
end;

:: deftheorem Def1 defines is_an_xrep_of PRGCOR_2:def_1_:_
 for D being non empty set
for p being XFinSequence of
for q being FinSequence of D holds
( p is_an_xrep_of q iff ( NAT c= D & p . 0 = len q & len q < len p & ( for i being Nat st 1 <= i & i <= len q holds
p . i = q . i ) ) );

theorem :: PRGCOR_2:1
for D being non empty set
for p being XFinSequence of st NAT c= D & p . 0 is Nat & p . 0 in len p holds
p is_an_xrep_of XFS2FS* p
proof
let D be non empty set ; ::_thesis: for p being XFinSequence of st NAT c= D & p . 0 is Nat & p . 0 in len p holds
p is_an_xrep_of XFS2FS* p
let p be XFinSequence of ; ::_thesis: ( NAT c= D & p . 0 is Nat & p . 0 in len p implies p is_an_xrep_of XFS2FS* p )
assume that
A1: NAT c= D and
A2: p . 0 is Nat and
A3: p . 0 in len p ; ::_thesis: p is_an_xrep_of XFS2FS* p
reconsider m0 = p . 0 as Nat by A2;
A4: m0 < len p by A3, NAT_1:44;
 ( len (XFS2FS* p) = m0 & ( for i being Nat st 1 <= i & i <= m0 holds
(XFS2FS* p) . i = p . i ) ) by A3, AFINSQ_1:def_11;
hence  p is_an_xrep_of XFS2FS* p by A1, A4, Def1; ::_thesis: verum
end;

definition
let x, y, a, b, c be set ;
func IFLGT (x,y,a,b,c) ->  set  equals :Def2: :: PRGCOR_2:def 2
a if x in y
b if x = y
otherwise c;
correctness
coherence
( ( x in y implies a is set ) & ( x = y implies b is set ) & ( not x in y & not x = y implies c is set ) );
consistency
for b1 being set st x in y & x = y holds
( b1 = a iff b1 = b );
;
end;

:: deftheorem Def2 defines IFLGT PRGCOR_2:def_2_:_
 for x, y, a, b, c being set holds
( ( x in y implies IFLGT (x,y,a,b,c) = a ) & ( x = y implies IFLGT (x,y,a,b,c) = b ) & ( not x in y & not x = y implies IFLGT (x,y,a,b,c) = c ) );

theorem Th2: :: PRGCOR_2:2
for D being non empty set
for q being FinSequence of D
for n being Nat st NAT c= D & n > len q holds
ex p being XFinSequence of st
( len p = n & p is_an_xrep_of q )
proof
let D be non empty set ; ::_thesis: for q being FinSequence of D
for n being Nat st NAT c= D & n > len q holds
ex p being XFinSequence of st
( len p = n & p is_an_xrep_of q )
let q be FinSequence of D; ::_thesis: for n being Nat st NAT c= D & n > len q holds
ex p being XFinSequence of st
( len p = n & p is_an_xrep_of q )
let n be Nat; ::_thesis: ( NAT c= D & n > len q implies ex p being XFinSequence of st
( len p = n & p is_an_xrep_of q ) )
assume that
A1: NAT c= D and
A2: n > len q ; ::_thesis: ex p being XFinSequence of st
( len p = n & p is_an_xrep_of q )
reconsider n = n as Element of NAT by ORDINAL1:def_12;
 len q in NAT ;
then consider d2 being set  such that
A3: d2 in D and
A4: d2 = len q by A1;
reconsider d = d2 as Element of D by A3;
deffunc H1( set ) ->  set = IFEQ ($1,0,d,(IFLGT ($1,(len q),(q . $1),(q . $1),d)));
 ex p being XFinSequence st
( len p = n & ( for k being Nat st k in n holds
p . k = H1(k) ) ) from AFINSQ_1:sch_2();
then consider p being XFinSequence such that
A5: len p = n and
A6: for k being Nat st k in n holds
p . k = H1(k) ;
 rng p c= D
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in D )
assume  y in rng p ; ::_thesis: y in D
then consider x being set  such that
A7: x in dom p and
A8: y = p . x by FUNCT_1:def_3;
reconsider nx = x as Ordinal by A7;
reconsider kx = nx as Element of NAT by A7;
A9: p . kx = H1(kx) by A5, A6, A7;
now__::_thesis:_(_(_x_=_0_&_p_._x_in_D_)_or_(_x_<>_0_&_p_._x_in_D_)_)
percases ( x = 0 or x <> 0 ) ;
case x = 0 ; ::_thesis: p . x in D
then  H1(x) = d by FUNCOP_1:def_8;
hence  p . x in D by A9; ::_thesis: verum
end;
caseA10: x <> 0 ; ::_thesis: p . x in D
then A11: H1(x) = IFLGT (x,(len q),(q . x),(q . x),d) by FUNCOP_1:def_8;
now__::_thesis:_(_(_x_in_len_q_&_p_._x_in_D_)_or_(_x_=_len_q_&_p_._x_in_D_)_or_(_not_x_in_len_q_&_not_x_=_len_q_&_p_._x_in_D_)_)
percases ( x in len q or x = len q or ( not x in len q & not x = len q ) ) ;
caseA12: x in len q ; ::_thesis: p . x in D
then A13: kx < len q by NAT_1:44;
 0 + 1 <= kx by A10, NAT_1:13;
then  kx in Seg (len q) by A13, FINSEQ_1:1;
then  x in dom q by FINSEQ_1:def_3;
then A14: q . x in rng q by FUNCT_1:def_3;
A15: rng q c= D by FINSEQ_1:def_4;
 H1(x) = q . x by A11, A12, Def2;
hence  p . x in D by A9, A14, A15; ::_thesis: verum
end;
caseA16: x = len q ; ::_thesis: p . x in D
 0 + 1 <= kx by A10, NAT_1:13;
then  kx in Seg (len q) by A16, FINSEQ_1:1;
then  x in dom q by FINSEQ_1:def_3;
then A17: q . x in rng q by FUNCT_1:def_3;
A18: rng q c= D by FINSEQ_1:def_4;
 H1(x) = q . x by A11, A16, Def2;
hence  p . x in D by A9, A17, A18; ::_thesis: verum
end;
case ( not x in len q & not x = len q ) ; ::_thesis: p . x in D
then  H1(x) = d by A11, Def2;
hence  p . x in D by A9; ::_thesis: verum
end;
end;
end;
hence  p . x in D ; ::_thesis: verum
end;
end;
end;
hence  y in D by A8; ::_thesis: verum
end;
then reconsider p = p as XFinSequence of by RELAT_1:def_19;
reconsider p2 = Replace (p,0,d) as XFinSequence of ;
A19: for i being Nat st 1 <= i & i <= len q holds
p2 . i = q . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len q implies p2 . i = q . i )
assume that
A20: 1 <= i and
A21: i <= len q ; ::_thesis: p2 . i = q . i
 ( i < len q or i = len q ) by A21, XXREAL_0:1;
then A22: ( i in len q or i = len q ) by NAT_1:44;
 i < n by A2, A21, XXREAL_0:2;
then A23: i in n by NAT_1:44;
 i in NAT by ORDINAL1:def_12;
hence p2 . i = p . i by A20, AFINSQ_1:44
.= H1(i) by A6, A23
.= IFLGT (i,(len q),(q . i),(q . i),d) by A20, FUNCOP_1:def_8
.= q . i by A22, Def2 ;
::_thesis: verum
end;
A24: len p2 = len p by AFINSQ_1:44;
 p2 . 0 = len q by A2, A4, A5, AFINSQ_1:44;
then  p2 is_an_xrep_of q by A1, A2, A5, A24, A19, Def1;
hence  ex p being XFinSequence of st
( len p = n & p is_an_xrep_of q ) by A5, A24; ::_thesis: verum
end;

definition
let a, b be XFinSequence of ;
assume that
A1: b . 0 is Nat and
A2: b . 0 < len a ;
func inner_prd_prg (a,b) ->  Real means :Def3: :: PRGCOR_2:def 3
 ex s being XFinSequence of ex n being Integer st
( len s = len a & s . 0 = 0 & n = b . 0 & ( n <> 0 implies for i being Nat st i < n holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & it = s . n );
existence
 ex b1 being Real ex s being XFinSequence of ex n being Integer st
( len s = len a & s . 0 = 0 & n = b . 0 & ( n <> 0 implies for i being Nat st i < n holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & b1 = s . n )
proof
reconsider q0 = <%0%> as XFinSequence of ;
set n2 = len a;
reconsider nn2 = b . 0 as Nat by A1;
reconsider nn = nn2 as Integer ;
defpred S1[ Nat] means  ex q being XFinSequence of st
( len q = $1 + 1 & q . 0 = 0 & ( for k being Nat st k < $1 & k < nn2 holds
q . (k + 1) = (q . k) + ((a . (k + 1)) * (b . (k + 1))) ) );
A3: for k being Nat st k < 0 & k < nn2 holds
q0 . (k + 1) = (q0 . k) + ((a . (k + 1)) * (b . (k + 1))) ;
A4: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
reconsider k0 = k as Nat ;
assume  S1[k] ; ::_thesis: S1[k + 1]
then consider q2 being XFinSequence of  such that
A5: len q2 = k + 1 and
A6: q2 . 0 = 0 and
A7: for k2 being Nat st k2 < k & k2 < nn2 holds
q2 . (k2 + 1) = (q2 . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) ;
reconsider qab = (q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))) as Real ;
set q3 = q2 ^ <%qab%>;
 0 in len q2 by A5, NAT_1:44;
then A8: (q2 ^ <%qab%>) . 0 = 0 by A6, AFINSQ_1:def_3;
A9: for k2 being Nat st k2 < k + 1 & k2 < nn2 holds
(q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1)))
proof
let k2 be Nat; ::_thesis: ( k2 < k + 1 & k2 < nn2 implies (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) )
assume that
A10: k2 < k + 1 and
A11: k2 < nn2 ; ::_thesis: (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1)))
A12: k2 <= k by A10, NAT_1:13;
now__::_thesis:_(_(_k2_<_k_&_(q2_^_<%qab%>)_._(k2_+_1)_=_((q2_^_<%qab%>)_._k2)_+_((a_._(k2_+_1))_*_(b_._(k2_+_1)))_)_or_(_k2_=_k_&_(q2_^_<%qab%>)_._(k2_+_1)_=_((q2_^_<%qab%>)_._k2)_+_((a_._(k2_+_1))_*_(b_._(k2_+_1)))_)_)
percases ( k2 < k or k2 = k ) by A12, XXREAL_0:1;
caseA13: k2 < k ; ::_thesis: (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1)))
then  k2 < len q2 by A5, NAT_1:13;
then  k2 in dom q2 by NAT_1:44;
then A14: (q2 ^ <%qab%>) . k2 = q2 . k2 by AFINSQ_1:def_3;
 k2 + 1 < k + 1 by A13, XREAL_1:6;
then  k2 + 1 in len q2 by A5, NAT_1:44;
then  (q2 ^ <%qab%>) . (k2 + 1) = q2 . (k2 + 1) by AFINSQ_1:def_3;
hence  (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) by A7, A11, A13, A14; ::_thesis: verum
end;
caseA15: k2 = k ; ::_thesis: (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1)))
 0 in 1 by NAT_1:44;
then  ( <%((q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))))%> . 0 = (q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))) & 0 in dom <%((q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))))%> ) by AFINSQ_1:def_4;
then A16: (q2 ^ <%qab%>) . ((k2 + 1) + 0) = (q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))) by A5, A15, AFINSQ_1:def_3;
 k2 < k2 + 1 by NAT_1:13;
then  k2 in dom q2 by A5, A15, NAT_1:44;
hence  (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) by A15, A16, AFINSQ_1:def_3; ::_thesis: verum
end;
end;
end;
hence  (q2 ^ <%qab%>) . (k2 + 1) = ((q2 ^ <%qab%>) . k2) + ((a . (k2 + 1)) * (b . (k2 + 1))) ; ::_thesis: verum
end;
len (q2 ^ <%qab%>) = (len q2) + (len <%((q2 . k0) + ((a . (k0 + 1)) * (b . (k0 + 1))))%>) by AFINSQ_1:17
.= (k + 1) + 1 by A5, AFINSQ_1:33 ;
hence  S1[k + 1] by A8, A9; ::_thesis: verum
end;
 ( len q0 = 1 & q0 . 0 = 0 ) by AFINSQ_1:def_4;
then A17: S1[ 0 ] by A3;
 for k being Nat holds S1[k] from NAT_1:sch_2(A17, A4);
then consider q being XFinSequence of  such that
A18: ( len q = ((len a) -' 1) + 1 & q . 0 = 0 ) and
A19: for k3 being Nat st k3 < (len a) -' 1 & k3 < nn2 holds
q . (k3 + 1) = (q . k3) + ((a . (k3 + 1)) * (b . (k3 + 1))) ;
reconsider ss2 = q . nn2 as Real ;
 len a >= 0 + 1 by A1, A2, NAT_1:13;
then  (len a) - 1 >= 0 by XREAL_1:48;
then A20: (len a) -' 1 = (len a) - 1 by XREAL_0:def_2;
 ( nn <> 0 implies for i being Nat st i < nn holds
q . (i + 1) = (q . i) + ((a . (i + 1)) * (b . (i + 1))) )
proof
assume  nn <> 0 ; ::_thesis: for i being Nat st i < nn holds
q . (i + 1) = (q . i) + ((a . (i + 1)) * (b . (i + 1)))
thus  for i being Nat st i < nn holds
q . (i + 1) = (q . i) + ((a . (i + 1)) * (b . (i + 1))) ::_thesis: verum
proof
let i be Nat; ::_thesis: ( i < nn implies q . (i + 1) = (q . i) + ((a . (i + 1)) * (b . (i + 1))) )
assume A21: i < nn ; ::_thesis: q . (i + 1) = (q . i) + ((a . (i + 1)) * (b . (i + 1)))
 nn + 1 <= len a by A2, NAT_1:13;
then  (nn + 1) - 1 <= (len a) - 1 by XREAL_1:9;
then  i < (len a) -' 1 by A20, A21, XXREAL_0:2;
hence  q . (i + 1) = (q . i) + ((a . (i + 1)) * (b . (i + 1))) by A19, A21; ::_thesis: verum
end;
end;
then  ex s being XFinSequence of ex n being Integer st
( len s = len a & s . 0 = 0 & n = b . 0 & ( n <> 0 implies for i being Nat st i < n holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & ss2 = s . n ) by A18, A20;
hence  ex b1 being Real ex s being XFinSequence of ex n being Integer st
( len s = len a & s . 0 = 0 & n = b . 0 & ( n <> 0 implies for i being Nat st i < n holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & b1 = s . n ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Real st ex s being XFinSequence of ex n being Integer st
( len s = len a & s . 0 = 0 & n = b . 0 & ( n <> 0 implies for i being Nat st i < n holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & b1 = s . n ) & ex s being XFinSequence of ex n being Integer st
( len s = len a & s . 0 = 0 & n = b . 0 & ( n <> 0 implies for i being Nat st i < n holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & b2 = s . n ) holds
b1 = b2
proof
thus  for w1, w2 being Real st ex s being XFinSequence of ex n1 being Integer st
( len s = len a & s . 0 = 0 & n1 = b . 0 & ( n1 <> 0 implies for i being Nat st i < n1 holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & w1 = s . n1 ) & ex s being XFinSequence of ex n2 being Integer st
( len s = len a & s . 0 = 0 & n2 = b . 0 & ( n2 <> 0 implies for i being Nat st i < n2 holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & w2 = s . n2 ) holds
w1 = w2 ::_thesis: verum
proof
let w1, w2 be Real; ::_thesis: ( ex s being XFinSequence of ex n1 being Integer st
( len s = len a & s . 0 = 0 & n1 = b . 0 & ( n1 <> 0 implies for i being Nat st i < n1 holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & w1 = s . n1 ) & ex s being XFinSequence of ex n2 being Integer st
( len s = len a & s . 0 = 0 & n2 = b . 0 & ( n2 <> 0 implies for i being Nat st i < n2 holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & w2 = s . n2 ) implies w1 = w2 )
assume that
A22: ex s being XFinSequence of ex n1 being Integer st
( len s = len a & s . 0 = 0 & n1 = b . 0 & ( n1 <> 0 implies for i being Nat st i < n1 holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & w1 = s . n1 ) and
A23: ex s being XFinSequence of ex n2 being Integer st
( len s = len a & s . 0 = 0 & n2 = b . 0 & ( n2 <> 0 implies for i being Nat st i < n2 holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & w2 = s . n2 ) ; ::_thesis: w1 = w2
consider s1 being XFinSequence of , n1 being Integer such that
 len s1 = len a and
A24: s1 . 0 = 0 and
A25: n1 = b . 0 and
A26: ( n1 <> 0 implies for i being Nat st i < n1 holds
s1 . (i + 1) = (s1 . i) + ((a . (i + 1)) * (b . (i + 1))) ) and
A27: w1 = s1 . n1 by A22;
consider s2 being XFinSequence of , n2 being Integer such that
 len s2 = len a and
A28: s2 . 0 = 0 and
A29: n2 = b . 0 and
A30: ( n2 <> 0 implies for i being Nat st i < n2 holds
s2 . (i + 1) = (s2 . i) + ((a . (i + 1)) * (b . (i + 1))) ) and
A31: w2 = s2 . n2 by A23;
reconsider n = n1 as Nat by A1, A25;
defpred S1[ Nat] means ( $1 <= n implies s1 . $1 = s2 . $1 );
A32: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A33: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_(_k_+_1_<=_n_implies_s1_._(k_+_1)_=_s2_._(k_+_1)_)
assume  k + 1 <= n ; ::_thesis: s1 . (k + 1) = s2 . (k + 1)
then A34: k < n by NAT_1:13;
then  s1 . (k + 1) = (s1 . k) + ((a . (k + 1)) * (b . (k + 1))) by A26;
hence  s1 . (k + 1) = s2 . (k + 1) by A25, A29, A30, A33, A34; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
A35: S1[ 0 ] by A24, A28;
 for k being Nat holds S1[k] from NAT_1:sch_2(A35, A32);
hence  w1 = w2 by A25, A27, A29, A31; ::_thesis: verum
end;
end;
end;

:: deftheorem Def3 defines inner_prd_prg PRGCOR_2:def_3_:_
 for a, b being XFinSequence of st b . 0 is Nat & b . 0 < len a holds
for b3 being Real holds
( b3 = inner_prd_prg (a,b) iff ex s being XFinSequence of ex n being Integer st
( len s = len a & s . 0 = 0 & n = b . 0 & ( n <> 0 implies for i being Nat st i < n holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & b3 = s . n ) );

theorem Th3: :: PRGCOR_2:3
for a being FinSequence of REAL
for s being XFinSequence of st s . 0 = 0 & ( for i being Nat st i < len a holds
s . (i + 1) = (s . i) + (a . (i + 1)) ) holds
Sum a = s . (len a)
proof
let a be FinSequence of REAL ; ::_thesis: for s being XFinSequence of st s . 0 = 0 & ( for i being Nat st i < len a holds
s . (i + 1) = (s . i) + (a . (i + 1)) ) holds
Sum a = s . (len a)
let s be XFinSequence of ; ::_thesis: ( s . 0 = 0 & ( for i being Nat st i < len a holds
s . (i + 1) = (s . i) + (a . (i + 1)) ) implies Sum a = s . (len a) )
assume that
A1: s . 0 = 0 and
A2: for i being Nat st i < len a holds
s . (i + 1) = (s . i) + (a . (i + 1)) ; ::_thesis: Sum a = s . (len a)
defpred S1[ Nat] means ( $1 <= len a implies Sum (a | $1) = s . $1 );
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
reconsider k1 = k as Element of NAT by ORDINAL1:def_12;
reconsider m = k1 + 1 as Nat ;
assume A4: S1[k] ; ::_thesis: S1[k + 1]
 ( k + 1 <= len a implies Sum (a | m) = s . (k + 1) )
proof
reconsider x0 = <*(a /. m)*> as FinSequence of REAL ;
reconsider rx = a /. m as Element of REAL ;
reconsider q0 = a | k as FinSequence of REAL ;
assume A5: k + 1 <= len a ; ::_thesis: Sum (a | m) = s . (k + 1)
then A6: a | m = (a | k) ^ <*(a /. m)*> by FINSEQ_5:82;
A7: 1 <= k + 1 by NAT_1:11;
then  m in Seg (len a) by A5, FINSEQ_1:1;
then A8: m in dom a by FINSEQ_1:def_3;
 m in Seg m by A7, FINSEQ_1:1;
then  m in Seg (len (a | m)) by A5, FINSEQ_1:59;
then A9: m in dom (a | m) by FINSEQ_1:def_3;
 Sum x0 = rx by RVSUM_1:73;
then A10: Sum (a | m) = (s . k) + rx by A4, A5, A6, NAT_1:13, RVSUM_1:75;
A11: len (a | m) = m by A5, FINSEQ_1:59;
A12: k < len a by A5, NAT_1:13;
len (a | m) = (len q0) + (len <*rx*>) by A6, FINSEQ_1:22
.= (len q0) + 1 by FINSEQ_1:40 ;
then rx = (a | m) . m by A6, A11, FINSEQ_1:42
.= (a | m) /. m by A9, PARTFUN1:def_6
.= a /. m by A9, FINSEQ_4:70
.= a . m by A8, PARTFUN1:def_6 ;
hence  Sum (a | m) = s . (k + 1) by A2, A12, A10; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
A13: S1[ 0 ] by A1, RVSUM_1:72;
 for k being Nat holds S1[k] from NAT_1:sch_2(A13, A3);
then  S1[ len a] ;
hence  Sum a = s . (len a) by FINSEQ_1:58; ::_thesis: verum
end;

theorem :: PRGCOR_2:4
for a being FinSequence of REAL ex s being XFinSequence of st
( len s = (len a) + 1 & s . 0 = 0 & ( for i being Nat st i < len a holds
s . (i + 1) = (s . i) + (a . (i + 1)) ) & Sum a = s . (len a) )
proof
let a be FinSequence of REAL ; ::_thesis: ex s being XFinSequence of st
( len s = (len a) + 1 & s . 0 = 0 & ( for i being Nat st i < len a holds
s . (i + 1) = (s . i) + (a . (i + 1)) ) & Sum a = s . (len a) )
deffunc H1( Nat) ->  Element of REAL = Sum (a | $1);
 ex p being XFinSequence st
( len p = (len a) + 1 & ( for k being Nat st k in (len a) + 1 holds
p . k = H1(k) ) ) from AFINSQ_1:sch_2();
then consider p being XFinSequence such that
A1: len p = (len a) + 1 and
A2: for k being Nat st k in (len a) + 1 holds
p . k = H1(k) ;
 rng p c= REAL
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in REAL )
assume  y in rng p ; ::_thesis: y in REAL
then consider x being set  such that
A3: x in dom p and
A4: y = p . x by FUNCT_1:def_3;
reconsider nx = x as Element of NAT by A3;
 p . nx = Sum (a | nx) by A1, A2, A3;
hence  y in REAL by A4; ::_thesis: verum
end;
then reconsider p = p as XFinSequence of by RELAT_1:def_19;
A5: for i being Nat st i < len a holds
p . (i + 1) = (p . i) + (a . (i + 1))
proof
let i be Nat; ::_thesis: ( i < len a implies p . (i + 1) = (p . i) + (a . (i + 1)) )
assume A6: i < len a ; ::_thesis: p . (i + 1) = (p . i) + (a . (i + 1))
reconsider i = i as Element of NAT by ORDINAL1:def_12;
reconsider ii = i + 1 as Nat ;
A7: i + 1 <= len a by A6, NAT_1:13;
 1 <= 1 + i by NAT_1:11;
then  i + 1 in Seg (len a) by A7, FINSEQ_1:1;
then A8: i + 1 in dom a by FINSEQ_1:def_3;
 i < (len a) + 1 by A6, NAT_1:13;
then  i in (len a) + 1 by NAT_1:44;
then A9: p . i = Sum (a | i) by A2;
 i + 1 < (len a) + 1 by A6, XREAL_1:6;
then A10: i + 1 in (len a) + 1 by NAT_1:44;
 a | ii = (a | i) ^ <*(a /. ii)*> by A7, FINSEQ_5:82;
then  Sum (a | ii) = (Sum (a | i)) + (Sum <*(a /. ii)*>) by RVSUM_1:75
.= (p . i) + (a /. ii) by A9, RVSUM_1:73
.= (p . i) + (a . ii) by A8, PARTFUN1:def_6 ;
hence  p . (i + 1) = (p . i) + (a . (i + 1)) by A2, A10; ::_thesis: verum
end;
 0 in (len a) + 1 by NAT_1:44;
then A11: p . 0 = H1( 0 ) by A2
.= 0 by RVSUM_1:72 ;
then  Sum a = p . (len a) by A5, Th3;
hence  ex s being XFinSequence of st
( len s = (len a) + 1 & s . 0 = 0 & ( for i being Nat st i < len a holds
s . (i + 1) = (s . i) + (a . (i + 1)) ) & Sum a = s . (len a) ) by A1, A11, A5; ::_thesis: verum
end;

theorem :: PRGCOR_2:5
for a, b being FinSequence of REAL
for n being Nat st len a = len b & n > len a holds
|(a,b)| = inner_prd_prg ((FS2XFS* (a,n)),(FS2XFS* (b,n)))
proof
let a, b be FinSequence of REAL ; ::_thesis: for n being Nat st len a = len b & n > len a holds
|(a,b)| = inner_prd_prg ((FS2XFS* (a,n)),(FS2XFS* (b,n)))
let n2 be Nat; ::_thesis: ( len a = len b & n2 > len a implies |(a,b)| = inner_prd_prg ((FS2XFS* (a,n2)),(FS2XFS* (b,n2))) )
assume that
A1: len a = len b and
A2: n2 > len a ; ::_thesis: |(a,b)| = inner_prd_prg ((FS2XFS* (a,n2)),(FS2XFS* (b,n2)))
reconsider rb = b as Element of (len a) -tuples_on REAL by A1, FINSEQ_2:92;
reconsider ra = a as Element of (len a) -tuples_on REAL by FINSEQ_2:92;
set ri = inner_prd_prg ((FS2XFS* (a,n2)),(FS2XFS* (b,n2)));
set pa = FS2XFS* (a,n2);
set pb = FS2XFS* (b,n2);
A3: len b = (FS2XFS* (b,n2)) . 0 by A1, A2, AFINSQ_1:def_10;
 len (FS2XFS* (a,n2)) = n2 by A2, AFINSQ_1:def_10;
then consider s being XFinSequence of , n being Integer such that
 len s = len (FS2XFS* (a,n2)) and
A4: s . 0 = 0 and
A5: n = (FS2XFS* (b,n2)) . 0 and
A6: ( n <> 0 implies for i being Nat st i < n holds
s . (i + 1) = (s . i) + (((FS2XFS* (a,n2)) . (i + 1)) * ((FS2XFS* (b,n2)) . (i + 1))) ) and
A7: inner_prd_prg ((FS2XFS* (a,n2)),(FS2XFS* (b,n2))) = s . n by A1, A2, A3, Def3;
A8: len (mlt (ra,rb)) = len a by CARD_1:def_7;
 for i being Nat st i < len (mlt (a,b)) holds
s . (i + 1) = (s . i) + ((mlt (a,b)) . (i + 1))
proof
let i be Nat; ::_thesis: ( i < len (mlt (a,b)) implies s . (i + 1) = (s . i) + ((mlt (a,b)) . (i + 1)) )
assume A9: i < len (mlt (a,b)) ; ::_thesis: s . (i + 1) = (s . i) + ((mlt (a,b)) . (i + 1))
then  ( 1 <= i + 1 & i + 1 <= len a ) by A8, NAT_1:11, NAT_1:13;
then A10: ( (FS2XFS* (a,n2)) . (i + 1) = a . (i + 1) & (FS2XFS* (b,n2)) . (i + 1) = b . (i + 1) ) by A1, A2, AFINSQ_1:def_10;
A11: i < n by A1, A2, A5, A8, A9, AFINSQ_1:def_10;
now__::_thesis:_(_(_n_<>_0_&_s_._(i_+_1)_=_(s_._i)_+_((mlt_(a,b))_._(i_+_1))_)_or_(_n_=_0_&_contradiction_)_)
percases ( n <> 0 or n = 0 ) ;
case n <> 0 ; ::_thesis: s . (i + 1) = (s . i) + ((mlt (a,b)) . (i + 1))
s . (i + 1) = (s . i) + (((FS2XFS* (a,n2)) . (i + 1)) * ((FS2XFS* (b,n2)) . (i + 1))) by A6, A11
.= (s . i) + ((mlt (a,b)) . (i + 1)) by A10, RVSUM_1:59 ;
hence  s . (i + 1) = (s . i) + ((mlt (a,b)) . (i + 1)) ; ::_thesis: verum
end;
case n = 0 ; ::_thesis: contradiction
hence  contradiction by A1, A2, A5, A8, A9, AFINSQ_1:def_10; ::_thesis: verum
end;
end;
end;
hence  s . (i + 1) = (s . i) + ((mlt (a,b)) . (i + 1)) ; ::_thesis: verum
end;
then  Sum (mlt (a,b)) = s . n by A1, A3, A4, A5, A8, Th3;
hence  |(a,b)| = inner_prd_prg ((FS2XFS* (a,n2)),(FS2XFS* (b,n2))) by A7, RVSUM_1:def_16; ::_thesis: verum
end;

definition
let b, c be XFinSequence of ;
let a be Real;
let m be Integer;
predm scalar_prd_prg c,a,b means :Def4: :: PRGCOR_2:def 4
( 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) ) ) );
end;

:: deftheorem Def4 defines scalar_prd_prg PRGCOR_2:def_4_:_
 for b, c being XFinSequence of
for a being Real
for m being Integer holds
( m scalar_prd_prg c,a,b iff ( 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) ) ) ) );

theorem :: PRGCOR_2:6
for b being non empty XFinSequence of
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 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) ) )
proof
let b be non empty XFinSequence of ; ::_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 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 & 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 & 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 that
A1: b . 0 is Nat and
A2: len b = m and
A3: 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) ) )
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 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  such that
A7: len p = m and
A8: p is_an_xrep_of c2 by A3, Th2;
reconsider p2 = Replace (p,0,(b . 0)) as XFinSequence of ;
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, Def1, 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, Def4;
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)
A13: 0 < len 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 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) ) by Def4;
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, Def4;
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)_)_)
percases ( 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, NAT_1:44;
then A23: k3 <= n by A15, A16, A21, AFINSQ_1:def_11;
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;
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;
end;

definition
let b, c be XFinSequence of ;
let m be Integer;
predm vector_minus_prg c,b means :Def5: :: PRGCOR_2:def 5
( 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 = - (b . i) ) ) );
end;

:: deftheorem Def5 defines vector_minus_prg PRGCOR_2:def_5_:_
 for b, c being XFinSequence of
for m being Integer holds
( m vector_minus_prg c,b iff ( 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 = - (b . i) ) ) ) );

theorem :: PRGCOR_2:7
for b being non empty XFinSequence of
for m being Nat st b . 0 is Nat & len b = m & b . 0 < m holds
( ex c being XFinSequence of st m vector_minus_prg c,b & ( for c being non empty XFinSequence of st m vector_minus_prg c,b holds
XFS2FS* c = - (XFS2FS* b) ) )
proof
let b be non empty XFinSequence of ; ::_thesis: for m being Nat st b . 0 is Nat & len b = m & b . 0 < m holds
( ex c being XFinSequence of st m vector_minus_prg c,b & ( for c being non empty XFinSequence of st m vector_minus_prg c,b holds
XFS2FS* c = - (XFS2FS* b) ) )
let m be Nat; ::_thesis: ( b . 0 is Nat & len b = m & b . 0 < m implies ( ex c being XFinSequence of st m vector_minus_prg c,b & ( for c being non empty XFinSequence of st m vector_minus_prg c,b holds
XFS2FS* c = - (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 st m vector_minus_prg c,b & ( for c being non empty XFinSequence of st m vector_minus_prg c,b holds
XFS2FS* c = - (XFS2FS* b) ) )
reconsider k = b . 0 as Nat by A1;
reconsider c2 = - (XFS2FS* b) as FinSequence of REAL ;
 dom (- (XFS2FS* b)) = dom (XFS2FS* b) by VALUED_1:8;
then A4: Seg (len (- (XFS2FS* b))) = dom (XFS2FS* b) by FINSEQ_1:def_3;
A5: b . 0 in 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  such that
A7: len p = m and
A8: p is_an_xrep_of c2 by A3, Th2;
reconsider p2 = Replace (p,0,(b . 0)) as XFinSequence of ;
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 A2, A5, A10, A11, AFINSQ_1:def_11;
then A12: (- (XFS2FS* b)) . i = - (b . i) by RVSUM_1:17;
 ( i in NAT & p . i = c2 . i ) by A6, A8, A10, A11, Def1, ORDINAL1:def_12;
hence  p2 . i = - (b . i) by A10, A12, AFINSQ_1:44; ::_thesis: verum
end;
 ( len p = len p2 & p2 . 0 = b . 0 ) by A1, A3, A7, AFINSQ_1:44;
then  m vector_minus_prg p2,b by A2, A7, A9, Def5;
hence  ex c being XFinSequence of st m vector_minus_prg c,b ; ::_thesis: for c being non empty XFinSequence of st m vector_minus_prg c,b holds
XFS2FS* c = - (XFS2FS* b)
A13: 0 < len b ;
thus  for c being non empty XFinSequence of st m vector_minus_prg c,b holds
XFS2FS* c = - (XFS2FS* b) ::_thesis: verum
proof
let c be non empty XFinSequence of ; ::_thesis: ( m vector_minus_prg c,b implies XFS2FS* c = - (XFS2FS* b) )
assume A14: m vector_minus_prg c,b ; ::_thesis: XFS2FS* c = - (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 = - (b . i) ) by Def5;
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, Def5;
then A19: len (XFS2FS* c) = c . 0 by A5, AFINSQ_1:def_11;
now__::_thesis:_(_(_n_=_0_&_XFS2FS*_c_=_-_(XFS2FS*_b)_)_or_(_n_<>_0_&_XFS2FS*_c_=_-_(XFS2FS*_b)_)_)
percases ( n = 0 or n <> 0 ) ;
caseA20: n = 0 ; ::_thesis: XFS2FS* c = - (XFS2FS* b)
then  XFS2FS* b = <*> REAL by A13, A16, AFINSQ_1:64;
hence  XFS2FS* c = - (XFS2FS* b) by A18, A16, A20, AFINSQ_1:64, RVSUM_1:19; ::_thesis: verum
end;
case n <> 0 ; ::_thesis: XFS2FS* c = - (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 )
A21: c . 0 in len c by A1, A3, A18, NAT_1:44;
then A22: len (XFS2FS* c) = n by A15, A16, AFINSQ_1:def_11;
assume A23: ( 1 <= k3 & k3 <= len (XFS2FS* c) ) ; ::_thesis: (XFS2FS* c) . k3 = c2 . k3
then A24: b . k3 = (XFS2FS* b) . k3 by A2, A5, A16, A22, AFINSQ_1:def_11;
(XFS2FS* c) . k3 = c . k3 by A15, A16, A23, A21, A22, AFINSQ_1:def_11
.= - (b . k3) by A17, A23, A22 ;
hence  (XFS2FS* c) . k3 = c2 . k3 by A24, RVSUM_1:17; ::_thesis: verum
end;
hence  XFS2FS* c = - (XFS2FS* b) by A6, A15, A19, FINSEQ_1:14; ::_thesis: verum
end;
end;
end;
hence  XFS2FS* c = - (XFS2FS* b) ; ::_thesis: verum
end;
end;

definition
let a, b, c be XFinSequence of ;
let m be Integer;
predm vector_add_prg c,a,b means :Def6: :: PRGCOR_2:def 6
( len c = m & len a = 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 . i) + (b . i) ) ) );
end;

:: deftheorem Def6 defines vector_add_prg PRGCOR_2:def_6_:_
 for a, b, c being XFinSequence of
for m being Integer holds
( m vector_add_prg c,a,b iff ( len c = m & len a = 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 . i) + (b . i) ) ) ) );

theorem :: PRGCOR_2:8
for a, b being non empty XFinSequence of
for m being Nat st b . 0 is Nat & len a = m & len b = m & a . 0 = b . 0 & b . 0 < m holds
( ex c being XFinSequence of st m vector_add_prg c,a,b & ( for c being non empty XFinSequence of st m vector_add_prg c,a,b holds
XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ) )
proof
let a, b be non empty XFinSequence of ; ::_thesis: for m being Nat st b . 0 is Nat & len a = m & len b = m & a . 0 = b . 0 & b . 0 < m holds
( ex c being XFinSequence of st m vector_add_prg c,a,b & ( for c being non empty XFinSequence of st m vector_add_prg c,a,b holds
XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ) )
let m be Nat; ::_thesis: ( b . 0 is Nat & len a = m & len b = m & a . 0 = b . 0 & b . 0 < m implies ( ex c being XFinSequence of st m vector_add_prg c,a,b & ( for c being non empty XFinSequence of st m vector_add_prg c,a,b holds
XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ) ) )
assume that
A1: b . 0 is Nat and
A2: len a = m and
A3: len b = m and
A4: a . 0 = b . 0 and
A5: b . 0 < m ; ::_thesis: ( ex c being XFinSequence of st m vector_add_prg c,a,b & ( for c being non empty XFinSequence of st m vector_add_prg c,a,b holds
XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ) )
reconsider k = b . 0 as Nat by A1;
reconsider Fb = XFS2FS* b as FinSequence of REAL ;
reconsider Fa = XFS2FS* a as FinSequence of REAL ;
reconsider c2 = Fa + Fb as FinSequence of REAL ;
A6: b . 0 in m by A1, A5, NAT_1:44;
then A7: len (XFS2FS* a) = b . 0 by A2, A4, AFINSQ_1:def_11;
A8: len (XFS2FS* b) = b . 0 by A3, A6, AFINSQ_1:def_11;
then A9: len c2 = len (XFS2FS* a) by A7, RVSUM_1:115;
then  dom c2 = Seg (len (XFS2FS* b)) by A8, A7, FINSEQ_1:def_3;
then  dom ((XFS2FS* a) + (XFS2FS* b)) = dom (XFS2FS* b) by FINSEQ_1:def_3;
then  Seg (len c2) = dom (XFS2FS* b) by FINSEQ_1:def_3;
then A10: len c2 = k by A8, FINSEQ_1:def_3;
then consider p being XFinSequence of  such that
A11: len p = m and
A12: p is_an_xrep_of c2 by A5, Th2;
reconsider p2 = Replace (p,0,(b . 0)) as XFinSequence of ;
A13: now__::_thesis:_(_k_<>_0_implies_for_i_being_Nat_st_1_<=_i_&_i_<=_k_holds_
p2_._i_=_(a_._i)_+_(b_._i)_)
assume  k <> 0 ; ::_thesis: for i being Nat st 1 <= i & i <= k holds
p2 . i = (a . i) + (b . i)
thus  for i being Nat st 1 <= i & i <= k holds
p2 . i = (a . i) + (b . i) ::_thesis: verum
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= k implies p2 . i = (a . i) + (b . i) )
assume that
A14: 1 <= i and
A15: i <= k ; ::_thesis: p2 . i = (a . i) + (b . i)
 i in Seg (len c2) by A7, A9, A14, A15, FINSEQ_1:1;
then A16: i in dom c2 by FINSEQ_1:def_3;
 ( (XFS2FS* a) . i = a . i & (XFS2FS* b) . i = b . i ) by A2, A3, A4, A6, A14, A15, AFINSQ_1:def_11;
then A17: ((XFS2FS* a) + (XFS2FS* b)) . i = (a . i) + (b . i) by A16, VALUED_1:def_1;
 ( i in NAT & p . i = c2 . i ) by A10, A12, A14, A15, Def1, ORDINAL1:def_12;
hence  p2 . i = (a . i) + (b . i) by A14, A17, AFINSQ_1:44; ::_thesis: verum
end;
end;
 ( len p = len p2 & p2 . 0 = b . 0 ) by A1, A5, A11, AFINSQ_1:44;
then  m vector_add_prg p2,a,b by A2, A3, A11, A13, Def6;
hence  ex c being XFinSequence of st m vector_add_prg c,a,b ; ::_thesis: for c being non empty XFinSequence of st m vector_add_prg c,a,b holds
XFS2FS* c = (XFS2FS* a) + (XFS2FS* b)
A18: 0 < len b ;
thus  for c being non empty XFinSequence of st m vector_add_prg c,a,b holds
XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ::_thesis: verum
proof
let c be non empty XFinSequence of ; ::_thesis: ( m vector_add_prg c,a,b implies XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) )
assume A19: m vector_add_prg c,a,b ; ::_thesis: XFS2FS* c = (XFS2FS* a) + (XFS2FS* b)
then consider n being Integer such that
A20: c . 0 = b . 0 and
A21: n = b . 0 and
A22: ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
c . i = (a . i) + (b . i) ) by Def6;
A23: ( 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 . i) + (b . i) ) ) ) by A19, Def6;
then A24: len (XFS2FS* c) = c . 0 by A6, AFINSQ_1:def_11;
now__::_thesis:_(_(_n_=_0_&_XFS2FS*_c_=_(XFS2FS*_a)_+_(XFS2FS*_b)_)_or_(_n_<>_0_&_XFS2FS*_c_=_(XFS2FS*_a)_+_(XFS2FS*_b)_)_)
percases ( n = 0 or n <> 0 ) ;
case n = 0 ; ::_thesis: XFS2FS* c = (XFS2FS* a) + (XFS2FS* b)
then  ( XFS2FS* b = <*> REAL & XFS2FS* c = <*> REAL ) by A18, A23, A21, AFINSQ_1:64;
hence  XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) by RVSUM_1:12; ::_thesis: verum
end;
case n <> 0 ; ::_thesis: XFS2FS* c = (XFS2FS* 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
A25: 1 <= k3 and
A26: k3 <= len (XFS2FS* c) ; ::_thesis: (XFS2FS* c) . k3 = c2 . k3
A27: c . 0 in len c by A1, A5, A23, NAT_1:44;
then A28: k3 <= n by A20, A21, A26, AFINSQ_1:def_11;
then A29: ( a . k3 = (XFS2FS* a) . k3 & b . k3 = (XFS2FS* b) . k3 ) by A2, A3, A4, A6, A21, A25, AFINSQ_1:def_11;
 k3 in Seg (len c2) by A10, A21, A25, A28, FINSEQ_1:1;
then A30: k3 in dom c2 by FINSEQ_1:def_3;
 len (XFS2FS* c) = n by A20, A21, A27, AFINSQ_1:def_11;
then (XFS2FS* c) . k3 = c . k3 by A20, A21, A25, A26, A27, AFINSQ_1:def_11
.= (a . k3) + (b . k3) by A22, A25, A28 ;
hence  (XFS2FS* c) . k3 = c2 . k3 by A30, A29, VALUED_1:def_1; ::_thesis: verum
end;
hence  XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) by A10, A20, A24, FINSEQ_1:14; ::_thesis: verum
end;
end;
end;
hence  XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ; ::_thesis: verum
end;
end;

definition
let a, b, c be XFinSequence of ;
let m be Integer;
predm vector_sub_prg c,a,b means :Def7: :: PRGCOR_2:def 7
( len c = m & len a = 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 . i) - (b . i) ) ) );
end;

:: deftheorem Def7 defines vector_sub_prg PRGCOR_2:def_7_:_
 for a, b, c being XFinSequence of
for m being Integer holds
( m vector_sub_prg c,a,b iff ( len c = m & len a = 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 . i) - (b . i) ) ) ) );

theorem :: PRGCOR_2:9
for a, b being non empty XFinSequence of
for m being Nat st b . 0 is Nat & len a = m & len b = m & a . 0 = b . 0 & b . 0 < m holds
( ex c being XFinSequence of st m vector_sub_prg c,a,b & ( for c being non empty XFinSequence of st m vector_sub_prg c,a,b holds
XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) ) )
proof
let a, b be non empty XFinSequence of ; ::_thesis: for m being Nat st b . 0 is Nat & len a = m & len b = m & a . 0 = b . 0 & b . 0 < m holds
( ex c being XFinSequence of st m vector_sub_prg c,a,b & ( for c being non empty XFinSequence of st m vector_sub_prg c,a,b holds
XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) ) )
let m be Nat; ::_thesis: ( b . 0 is Nat & len a = m & len b = m & a . 0 = b . 0 & b . 0 < m implies ( ex c being XFinSequence of st m vector_sub_prg c,a,b & ( for c being non empty XFinSequence of st m vector_sub_prg c,a,b holds
XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) ) ) )
assume that
A1: b . 0 is Nat and
A2: len a = m and
A3: len b = m and
A4: a . 0 = b . 0 and
A5: b . 0 < m ; ::_thesis: ( ex c being XFinSequence of st m vector_sub_prg c,a,b & ( for c being non empty XFinSequence of st m vector_sub_prg c,a,b holds
XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) ) )
reconsider k = b . 0 as Nat by A1;
reconsider Fb = XFS2FS* b as FinSequence of REAL ;
reconsider Fa = XFS2FS* a as FinSequence of REAL ;
reconsider c2 = Fa - Fb as FinSequence of REAL ;
A6: b . 0 in m by A1, A5, NAT_1:44;
then A7: len (XFS2FS* a) = b . 0 by A2, A4, AFINSQ_1:def_11;
A8: len (XFS2FS* b) = b . 0 by A3, A6, AFINSQ_1:def_11;
then A9: len c2 = len (XFS2FS* a) by A7, RVSUM_1:116;
then  dom c2 = Seg (len (XFS2FS* b)) by A8, A7, FINSEQ_1:def_3;
then  dom ((XFS2FS* a) - (XFS2FS* b)) = dom (XFS2FS* b) by FINSEQ_1:def_3;
then  Seg (len c2) = dom (XFS2FS* b) by FINSEQ_1:def_3;
then A10: len c2 = k by A8, FINSEQ_1:def_3;
then consider p being XFinSequence of  such that
A11: len p = m and
A12: p is_an_xrep_of c2 by A5, Th2;
reconsider p2 = Replace (p,0,(b . 0)) as XFinSequence of ;
A13: now__::_thesis:_(_k_<>_0_implies_for_i_being_Nat_st_1_<=_i_&_i_<=_k_holds_
p2_._i_=_(a_._i)_-_(b_._i)_)
assume  k <> 0 ; ::_thesis: for i being Nat st 1 <= i & i <= k holds
p2 . i = (a . i) - (b . i)
thus  for i being Nat st 1 <= i & i <= k holds
p2 . i = (a . i) - (b . i) ::_thesis: verum
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= k implies p2 . i = (a . i) - (b . i) )
assume that
A14: 1 <= i and
A15: i <= k ; ::_thesis: p2 . i = (a . i) - (b . i)
 i in Seg (len c2) by A7, A9, A14, A15, FINSEQ_1:1;
then A16: i in dom c2 by FINSEQ_1:def_3;
 ( (XFS2FS* a) . i = a . i & (XFS2FS* b) . i = b . i ) by A2, A3, A4, A6, A14, A15, AFINSQ_1:def_11;
then A17: ((XFS2FS* a) - (XFS2FS* b)) . i = (a . i) - (b . i) by A16, VALUED_1:13;
 ( i in NAT & p . i = c2 . i ) by A10, A12, A14, A15, Def1, ORDINAL1:def_12;
hence  p2 . i = (a . i) - (b . i) by A14, A17, AFINSQ_1:44; ::_thesis: verum
end;
end;
 ( len p = len p2 & p2 . 0 = b . 0 ) by A1, A5, A11, AFINSQ_1:44;
then  m vector_sub_prg p2,a,b by A2, A3, A11, A13, Def7;
hence  ex c being XFinSequence of st m vector_sub_prg c,a,b ; ::_thesis: for c being non empty XFinSequence of st m vector_sub_prg c,a,b holds
XFS2FS* c = (XFS2FS* a) - (XFS2FS* b)
A18: 0 < len b ;
thus  for c being non empty XFinSequence of st m vector_sub_prg c,a,b holds
XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) ::_thesis: verum
proof
let c be non empty XFinSequence of ; ::_thesis: ( m vector_sub_prg c,a,b implies XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) )
assume A19: m vector_sub_prg c,a,b ; ::_thesis: XFS2FS* c = (XFS2FS* a) - (XFS2FS* b)
then consider n being Integer such that
A20: c . 0 = b . 0 and
A21: n = b . 0 and
A22: ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
c . i = (a . i) - (b . i) ) by Def7;
A23: ( 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 . i) - (b . i) ) ) ) by A19, Def7;
then A24: len (XFS2FS* c) = c . 0 by A6, AFINSQ_1:def_11;
now__::_thesis:_(_(_n_=_0_&_XFS2FS*_c_=_(XFS2FS*_a)_-_(XFS2FS*_b)_)_or_(_n_<>_0_&_XFS2FS*_c_=_(XFS2FS*_a)_-_(XFS2FS*_b)_)_)
percases ( n = 0 or n <> 0 ) ;
case n = 0 ; ::_thesis: XFS2FS* c = (XFS2FS* a) - (XFS2FS* b)
then  ( XFS2FS* b = <*> REAL & XFS2FS* c = <*> REAL ) by A18, A23, A21, AFINSQ_1:64;
hence  XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) by RVSUM_1:28; ::_thesis: verum
end;
case n <> 0 ; ::_thesis: XFS2FS* c = (XFS2FS* 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
A25: 1 <= k3 and
A26: k3 <= len (XFS2FS* c) ; ::_thesis: (XFS2FS* c) . k3 = c2 . k3
A27: c . 0 in len c by A1, A5, A23, NAT_1:44;
then A28: k3 <= n by A20, A21, A26, AFINSQ_1:def_11;
then A29: ( a . k3 = (XFS2FS* a) . k3 & b . k3 = (XFS2FS* b) . k3 ) by A2, A3, A4, A6, A21, A25, AFINSQ_1:def_11;
 k3 in Seg (len c2) by A10, A21, A25, A28, FINSEQ_1:1;
then A30: k3 in dom c2 by FINSEQ_1:def_3;
A31: len (XFS2FS* c) = n by A20, A21, A27, AFINSQ_1:def_11;
then (XFS2FS* c) . k3 = c . k3 by A20, A21, A25, A26, A27, AFINSQ_1:def_11
.= (a . k3) - (b . k3) by A22, A25, A26, A31 ;
hence  (XFS2FS* c) . k3 = c2 . k3 by A30, A29, VALUED_1:13; ::_thesis: verum
end;
hence  XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) by A10, A20, A24, FINSEQ_1:14; ::_thesis: verum
end;
end;
end;
hence  XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) ; ::_thesis: verum
end;
end;