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: S₁[ 0 ]

proof

let R1, R2 be Element of 0 -tuples_on REAL ; :: thesis: (Sum (mlt R1,R2)) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2))
( sqr R1 = <*> REAL & mlt R1,R2 = <*> REAL ) by FINSEQ_2:113;
hence (Sum (mlt R1,R2)) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2)) by Th102; :: thesis: verum

end;

A2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: 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 R1' being Element of i -tuples_on REAL , x1 being Element of REAL such that
A4: R1 = R1' ^ <*x1*> by FINSEQ_2:137;
consider R2' being Element of i -tuples_on REAL , x2 being Element of REAL such that
A5: R2 = R2' ^ <*x2*> by FINSEQ_2:137;
((Sum (mlt R1',R2')) ^2 ) + 0 <= (Sum (sqr R1')) * (Sum (sqr R2')) by A3;
then A6: 0 <= ((Sum (sqr R1')) * (Sum (sqr R2'))) - ((Sum (mlt R1',R2')) ^2 ) by XREAL_1:21;
A7: ((Sum (sqr R1')) + (x1 ^2 )) * ((Sum (sqr R2')) + (x2 ^2 )) = (((Sum (sqr R1')) * (Sum (sqr R2'))) + (((x1 ^2 ) * (Sum (sqr R2'))) + ((Sum (sqr R1')) * (x2 ^2 )))) + ((x1 ^2 ) * (x2 ^2 ))
.= (((Sum (sqr R1')) * (Sum (sqr R2'))) + ((Sum ((x1 ^2 ) * (sqr R2'))) + ((Sum (sqr R1')) * (x2 ^2 )))) + ((x1 ^2 ) * (x2 ^2 )) by Th117
.= (((Sum (sqr R1')) * (Sum (sqr R2'))) + ((Sum (sqr (x1 * R2'))) + ((x2 ^2 ) * (Sum (sqr R1'))))) + ((x1 ^2 ) * (x2 ^2 )) by Th84
.= (((Sum (sqr R1')) * (Sum (sqr R2'))) + ((Sum (sqr (x1 * R2'))) + (Sum ((x2 ^2 ) * (sqr R1'))))) + ((x1 ^2 ) * (x2 ^2 )) by Th117
.= (((Sum (sqr R1')) * (Sum (sqr R2'))) + ((Sum (sqr (x1 * R2'))) + (Sum (sqr (x2 * R1'))))) + ((x1 ^2 ) * (x2 ^2 )) by Th84 ;
mlt (R1' ^ <*x1*>),(R2' ^ <*x2*>) = (multreal .: R1',R2') ^ <*(multreal . x1,x2)*> by FINSEQOP:11
.= (mlt R1',R2') ^ <*(x1 * x2)*> by BINOP_2:def 11 ;
then A8: Sum (mlt (R1' ^ <*x1*>),(R2' ^ <*x2*>)) = (Sum (mlt R1',R2')) + (x1 * x2) by Th104;
A9: (2 * (x1 * x2)) * (Sum (mlt R1',R2')) = 2 * ((x1 * x2) * (Sum (mlt R1',R2')))
.= 2 * (Sum ((x1 * x2) * (mlt R1',R2'))) by Th117
.= 2 * (Sum (x1 * (x2 * (mlt R1',R2')))) by Th71
.= 2 * (Sum (x1 * (mlt R2',(x2 * R1')))) by Th94
.= 2 * (Sum (mlt (x1 * R2'),(x2 * R1'))) by FINSEQOP:27 ;
A10: - (((Sum (mlt R1',R2')) + (x1 * x2)) ^2 ) = (- ((x1 * x2) ^2 )) + (- (((2 * (x1 * x2)) * (Sum (mlt R1',R2'))) + ((Sum (mlt R1',R2')) ^2 )))
.= (- ((x1 ^2 ) * (x2 ^2 ))) + ((- ((Sum (mlt R1',R2')) ^2 )) + (- (2 * (Sum (mlt (x1 * R2'),(x2 * R1')))))) by A9 ;
A11: ((Sum (sqr (x1 * R2'))) + (Sum (sqr (x2 * R1')))) + (- (2 * (Sum (mlt (x1 * R2'),(x2 * R1'))))) = ((Sum (sqr (x1 * R2'))) - (2 * (Sum (mlt (x1 * R2'),(x2 * R1'))))) + (Sum (sqr (x2 * R1')))
.= ((Sum (sqr (x1 * R2'))) - (Sum (2 * (mlt (x1 * R2'),(x2 * R1'))))) + (Sum (sqr (x2 * R1'))) by Th117
.= (Sum ((sqr (x1 * R2')) - (2 * (mlt (x1 * R2'),(x2 * R1'))))) + (Sum (sqr (x2 * R1'))) by Th120
.= Sum (((sqr (x1 * R2')) - (2 * (mlt (x1 * R2'),(x2 * R1')))) + (sqr (x2 * R1'))) by Th119 ;
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 ( (Sum (sqr R1')) + (x1 ^2 ) = Sum (sqr R1) & (Sum (sqr R2')) + (x2 ^2 ) = Sum (sqr R2) ) by A4, A5;
then A12: ((Sum (sqr R1)) * (Sum (sqr R2))) - ((Sum (mlt R1,R2)) ^2 ) = (((Sum (sqr R1')) + (x1 ^2 )) * ((Sum (sqr R2')) + (x2 ^2 ))) + (- (((Sum (mlt R1',R2')) + (x1 * x2)) ^2 )) by A4, A5, A8
.= (((Sum (sqr R1')) * (Sum (sqr R2'))) + (- ((Sum (mlt R1',R2')) ^2 ))) + (((Sum (sqr (x1 * R2'))) + (Sum (sqr (x2 * R1')))) + (- (2 * (Sum (mlt (x1 * R2'),(x2 * R1')))))) by A7, A10
.= (((Sum (sqr R1')) * (Sum (sqr R2'))) - ((Sum (mlt R1',R2')) ^2 )) + (Sum (sqr ((x1 * R2') - (x2 * R1')))) by A11, Th99 ;
0 <= Sum (sqr ((x1 * R2') - (x2 * R1'))) by Th116;
then 0 + 0 <= ((Sum (sqr R1)) * (Sum (sqr R2))) - ((Sum (mlt R1,R2)) ^2 ) by A6, A12, XREAL_1:9;
then ((Sum (mlt R1,R2)) ^2 ) + 0 <= (Sum (sqr R1)) * (Sum (sqr R2)) by XREAL_1:21;
hence (Sum (mlt R1,R2)) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2)) ; :: thesis: verum

end;

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