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:110;
reconsider ra = a as Element of (len a) -tuples_on REAL by FINSEQ_2:110;
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 11;
len (FS2XFS* a,n2) = n2 by A2, AFINSQ_1:def 11;
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, Def7;
A8: len (mlt ra,rb) = len a by FINSEQ_1:def 18;
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 A10: 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 A13: ( (FS2XFS* a,n2) . (i + 1) = a . (i + 1) & (FS2XFS* b,n2) . (i + 1) = b . (i + 1) ) by A1, A2, AFINSQ_1:def 11;
A14: i < n by A1, A2, A5, A8, A10, AFINSQ_1:def 11;

now

per cases ( 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, A14
.= (s . i) + ((mlt a,b) . (i + 1)) by A13, RVSUM_1:86 ;
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, A10, AFINSQ_1:def 11; :: 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, Th8;
hence |(a,b)| = inner_prd_prg (FS2XFS* a,n2),(FS2XFS* b,n2) by A7, RVSUM_1:def 17; :: thesis: verum