let x, y be real-valued FinSequence; :: thesis: ( len x = len y implies |.|(x,y)|.| <= |.x.| * |.y.| )
assume A1: len x = len y ; :: thesis: |.|(x,y)|.| <= |.x.| * |.y.|
A2: ( x = 0* (len x) implies |.|(x,y)|.| <= (sqrt |(x,x)|) * (sqrt |(y,y)|) )

proof

assume x = 0* (len x) ; :: thesis: |.|(x,y)|.| <= (sqrt |(x,x)|) * (sqrt |(y,y)|)
then ( |(x,y)| = 0 & |(x,x)| = 0 ) by A1, Th8;
hence |.|(x,y)|.| <= (sqrt |(x,x)|) * (sqrt |(y,y)|) by ABSVALUE:2; :: thesis: verum

end;

A3: ( x <> 0* (len x) implies |.|(x,y)|.| <= (sqrt |(x,x)|) * (sqrt |(y,y)|) )

proof

A4: for t being Real holds ((|(x,x)| * (t ^2)) + ((2 * |(x,y)|) * t)) + |(y,y)| >= 0

proof

let t be Real; :: thesis: ((|(x,x)| * (t ^2)) + ((2 * |(x,y)|) * t)) + |(y,y)| >= 0
set s = t ^2 ;
A5: len (t * x) = len x by RVSUM_1:117;
|(((t * x) + y),((t * x) + y))| >= 0 by RVSUM_1:119;
then (|((t * x),(t * x))| + (2 * |((t * x),y)|)) + |(y,y)| >= 0 by A1, A5, RVSUM_1:128;
then ((t * |((t * x),x)|) + (2 * |((t * x),y)|)) + |(y,y)| >= 0 by A5, RVSUM_1:121;
then ((t * (t * |(x,x)|)) + (2 * |((t * x),y)|)) + |(y,y)| >= 0 by A1, RVSUM_1:121;
then ((|(x,x)| * (t ^2)) + (2 * (|(x,y)| * t))) + |(y,y)| >= 0 by A1, RVSUM_1:121;
hence ((|(x,x)| * (t ^2)) + ((2 * |(x,y)|) * t)) + |(y,y)| >= 0 ; :: thesis: verum

end;

set w = |.|(x,y)|.|;
set u = |(x,y)|;
A6: |(x,x)| >= 0 by RVSUM_1:119;
assume x <> 0* (len x) ; :: thesis: |.|(x,y)|.| <= (sqrt |(x,x)|) * (sqrt |(y,y)|)
then |(x,x)| <> 0 by Th6;
then |(x,x)| > 0 by A6, XXREAL_0:1;
then delta (|(x,x)|,(2 * |(x,y)|),|(y,y)|) <= 0 by A4, QUIN_1:10;
then ((2 * |(x,y)|) ^2) - ((4 * |(x,x)|) * |(y,y)|) <= 0 by QUIN_1:def 1;
then 4 * ((|(x,y)| ^2) - (|(x,x)| * |(y,y)|)) <= 0 ;
then (|(x,y)| ^2) - (|(x,x)| * |(y,y)|) <= 0 / 4 by XREAL_1:77;
then |(x,y)| ^2 <= |(x,x)| * |(y,y)| by XREAL_1:50;
then ( 0 <= |.|(x,y)|.| ^2 & |.|(x,y)|.| ^2 <= |(x,x)| * |(y,y)| ) by COMPLEX1:75, XREAL_1:63;
then sqrt (|.|(x,y)|.| ^2) <= sqrt (|(x,x)| * |(y,y)|) by SQUARE_1:26;
then A7: |.|(x,y)|.| <= sqrt (|(x,x)| * |(y,y)|) by COMPLEX1:46, SQUARE_1:22;
|(y,y)| >= 0 by RVSUM_1:119;
hence |.|(x,y)|.| <= (sqrt |(x,x)|) * (sqrt |(y,y)|) by A6, A7, SQUARE_1:29; :: thesis: verum

end;

sqrt |(x,x)| = |.x.| by Th5;
hence |.|(x,y)|.| <= |.x.| * |.y.| by A2, A3, Th5; :: thesis: verum