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, NUMBERS:19;
len (FS2XFS* (a,n2)) = n2 by A2, AFINSQ_1:def 10, NUMBERS:19;
then consider s being XFinSequence of REAL , 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, NUMBERS:19;
A11: i < n by A1, A2, A5, A8, A9, AFINSQ_1:def 10, NUMBERS:19;

now :: thesis: ( ( n <> 0 & s . (i + 1) = (s . i) + ((mlt (a,b)) . (i + 1)) ) or ( n = 0 & contradiction ) )

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, 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, NUMBERS:19; :: 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