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

proof

assume x = 0* (len x) ; :: thesis: abs |(x,y)| <= (sqrt |(x,x)|) * (sqrt |(y,y)|)
then ( |(x,y)| = 0 & |(x,x)| = 0 ) by A1, Th17;
hence abs |(x,y)| <= (sqrt |(x,x)|) * (sqrt |(y,y)|) by ABSVALUE:7, SQUARE_1:82; :: thesis: verum

end;

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

proof

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

proof

let t be real number ; :: 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:147;
|(((t * x) + y),((t * x) + y))| >= 0 by RVSUM_1:149;
then (|((t * x),(t * x))| + (2 * |((t * x),y)|)) + |(y,y)| >= 0 by A1, A5, RVSUM_1:158;
then ((t * |((t * x),x)|) + (2 * |((t * x),y)|)) + |(y,y)| >= 0 by A5, RVSUM_1:151;
then ((t * (t * |(x,x)|)) + (2 * |((t * x),y)|)) + |(y,y)| >= 0 by A1, RVSUM_1:151;
then ((|(x,x)| * (t ^2 )) + (2 * (|(x,y)| * t))) + |(y,y)| >= 0 by A1, RVSUM_1:151;
hence ((|(x,x)| * (t ^2 )) + ((2 * |(x,y)|) * t)) + |(y,y)| >= 0 ; :: thesis: verum

end;

set w = abs |(x,y)|;
set u = |(x,y)|;
A6: |(x,x)| >= 0 by RVSUM_1:149;
assume x <> 0* (len x) ; :: thesis: abs |(x,y)| <= (sqrt |(x,x)|) * (sqrt |(y,y)|)
then |(x,x)| <> 0 by Th15;
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:79;
then |(x,y)| ^2 <= |(x,x)| * |(y,y)| by XREAL_1:52;
then ( 0 <= (abs |(x,y)|) ^2 & (abs |(x,y)|) ^2 <= |(x,x)| * |(y,y)| ) by COMPLEX1:161, XREAL_1:65;
then sqrt ((abs |(x,y)|) ^2 ) <= sqrt (|(x,x)| * |(y,y)|) by SQUARE_1:94;
then A7: abs |(x,y)| <= sqrt (|(x,x)| * |(y,y)|) by COMPLEX1:132, SQUARE_1:89;
|(y,y)| >= 0 by RVSUM_1:149;
hence abs |(x,y)| <= (sqrt |(x,x)|) * (sqrt |(y,y)|) by A6, A7, SQUARE_1:97; :: thesis: verum

end;

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