let i be Nat; :: thesis: for R1, R2 being Element of i -tuples_on REAL holds (Sum (mlt R1,R2)) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2))
let R1, R2 be Element of i -tuples_on REAL ; :: thesis: (Sum (mlt R1,R2)) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2))
defpred S₁[ Nat] means for R1, R2 being Element of $1 -tuples_on REAL holds (Sum (mlt R1,R2)) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2));
A1: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A2: for R1, R2 being Element of i -tuples_on REAL holds (Sum (mlt R1,R2)) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2)) ; :: thesis: S₁[i + 1]
let R1, R2 be Element of (i + 1) -tuples_on REAL ; :: thesis: (Sum (mlt R1,R2)) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2))
consider R19 being Element of i -tuples_on REAL , x1 being Element of REAL such that
A3: R1 = R19 ^ <*x1*> by FINSEQ_2:137;
consider R29 being Element of i -tuples_on REAL , x2 being Element of REAL such that
A4: R2 = R29 ^ <*x2*> by FINSEQ_2:137;
A5: for r being real number
for R being Element of i -tuples_on REAL holds Sum (sqr (R ^ <*r*>)) = (Sum (sqr R)) + (r ^2 )

proof

let r be real number ; :: thesis: for R being Element of i -tuples_on REAL holds Sum (sqr (R ^ <*r*>)) = (Sum (sqr R)) + (r ^2 )
let R be Element of i -tuples_on REAL ; :: thesis: Sum (sqr (R ^ <*r*>)) = (Sum (sqr R)) + (r ^2 )
reconsider s = r as Element of REAL by XREAL_0:def 1;
sqr (R ^ <*s*>) = (sqrreal * R) ^ <*(sqrreal . s)*> by FINSEQOP:9
.= (sqr R) ^ <*(r ^2 )*> by Def2 ;
hence Sum (sqr (R ^ <*r*>)) = (Sum (sqr R)) + (r ^2 ) by Th104; :: thesis: verum

end;

then A6: (Sum (sqr R29)) + (x2 ^2 ) = Sum (sqr R2) by A4;
((Sum (mlt R19,R29)) ^2 ) + 0 <= (Sum (sqr R19)) * (Sum (sqr R29)) by A2;
then A7: 0 <= ((Sum (sqr R19)) * (Sum (sqr R29))) - ((Sum (mlt R19,R29)) ^2 ) by XREAL_1:21;
mlt (R19 ^ <*x1*>),(R29 ^ <*x2*>) = (multreal .: R19,R29) ^ <*(multreal . x1,x2)*> by FINSEQOP:11
.= (mlt R19,R29) ^ <*(x1 * x2)*> by BINOP_2:def 11 ;
then A8: Sum (mlt (R19 ^ <*x1*>),(R29 ^ <*x2*>)) = (Sum (mlt R19,R29)) + (x1 * x2) by Th104;
A9: (2 * (x1 * x2)) * (Sum (mlt R19,R29)) = 2 * ((x1 * x2) * (Sum (mlt R19,R29)))
.= 2 * (Sum ((x1 * x2) * (mlt R19,R29))) by Th117
.= 2 * (Sum (x1 * (x2 * (mlt R19,R29)))) by RFUNCT_1:29
.= 2 * (Sum (x1 * (mlt R29,(x2 * R19)))) by RFUNCT_1:24
.= 2 * (Sum (mlt (x1 * R29),(x2 * R19))) by FINSEQOP:27 ;
A10: - (((Sum (mlt R19,R29)) + (x1 * x2)) ^2 ) = (- ((x1 * x2) ^2 )) + (- (((2 * (x1 * x2)) * (Sum (mlt R19,R29))) + ((Sum (mlt R19,R29)) ^2 )))
.= (- ((x1 ^2 ) * (x2 ^2 ))) + ((- ((Sum (mlt R19,R29)) ^2 )) + (- (2 * (Sum (mlt (x1 * R29),(x2 * R19)))))) by A9 ;
A11: 0 <= Sum (sqr ((x1 * R29) - (x2 * R19))) by Th116;
A12: ((Sum (sqr R19)) + (x1 ^2 )) * ((Sum (sqr R29)) + (x2 ^2 )) = (((Sum (sqr R19)) * (Sum (sqr R29))) + (((x1 ^2 ) * (Sum (sqr R29))) + ((Sum (sqr R19)) * (x2 ^2 )))) + ((x1 ^2 ) * (x2 ^2 ))
.= (((Sum (sqr R19)) * (Sum (sqr R29))) + ((Sum ((x1 ^2 ) * (sqr R29))) + ((Sum (sqr R19)) * (x2 ^2 )))) + ((x1 ^2 ) * (x2 ^2 )) by Th117
.= (((Sum (sqr R19)) * (Sum (sqr R29))) + ((Sum (sqr (x1 * R29))) + ((x2 ^2 ) * (Sum (sqr R19))))) + ((x1 ^2 ) * (x2 ^2 )) by Th84
.= (((Sum (sqr R19)) * (Sum (sqr R29))) + ((Sum (sqr (x1 * R29))) + (Sum ((x2 ^2 ) * (sqr R19))))) + ((x1 ^2 ) * (x2 ^2 )) by Th117
.= (((Sum (sqr R19)) * (Sum (sqr R29))) + ((Sum (sqr (x1 * R29))) + (Sum (sqr (x2 * R19))))) + ((x1 ^2 ) * (x2 ^2 )) by Th84 ;
A13: ((Sum (sqr (x1 * R29))) + (Sum (sqr (x2 * R19)))) + (- (2 * (Sum (mlt (x1 * R29),(x2 * R19))))) = ((Sum (sqr (x1 * R29))) - (2 * (Sum (mlt (x1 * R29),(x2 * R19))))) + (Sum (sqr (x2 * R19)))
.= ((Sum (sqr (x1 * R29))) - (Sum (2 * (mlt (x1 * R29),(x2 * R19))))) + (Sum (sqr (x2 * R19))) by Th117
.= (Sum ((sqr (x1 * R29)) - (2 * (mlt (x1 * R29),(x2 * R19))))) + (Sum (sqr (x2 * R19))) by Th120
.= Sum (((sqr (x1 * R29)) - (2 * (mlt (x1 * R29),(x2 * R19)))) + (sqr (x2 * R19))) by Th119 ;
(Sum (sqr R19)) + (x1 ^2 ) = Sum (sqr R1) by A3, A5;
then ((Sum (sqr R1)) * (Sum (sqr R2))) - ((Sum (mlt R1,R2)) ^2 ) = (((Sum (sqr R19)) + (x1 ^2 )) * ((Sum (sqr R29)) + (x2 ^2 ))) + (- (((Sum (mlt R19,R29)) + (x1 * x2)) ^2 )) by A3, A4, A8, A6
.= (((Sum (sqr R19)) * (Sum (sqr R29))) + (- ((Sum (mlt R19,R29)) ^2 ))) + (((Sum (sqr (x1 * R29))) + (Sum (sqr (x2 * R19)))) + (- (2 * (Sum (mlt (x1 * R29),(x2 * R19)))))) by A12, A10
.= (((Sum (sqr R19)) * (Sum (sqr R29))) - ((Sum (mlt R19,R29)) ^2 )) + (Sum (sqr ((x1 * R29) - (x2 * R19)))) by A13, Th99 ;
then ((Sum (mlt R1,R2)) ^2 ) + 0 <= (Sum (sqr R1)) * (Sum (sqr R2)) by XREAL_1:21, A7, A11;
hence (Sum (mlt R1,R2)) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2)) ; :: thesis: verum

end;

A14: S₁[ 0 ] ;
for i being Nat holds S₁[i] from NAT_1:sch 2(A14, A1);
hence (Sum (mlt R1,R2)) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2)) ; :: thesis: verum