let R be Ring; :: thesis: for a, b being Element of R st a is sum_of_squares & b is sum_of_squares holds
a + b is sum_of_squares
let a, b be Element of R; :: thesis: ( a is sum_of_squares & b is sum_of_squares implies a + b is sum_of_squares )
assume AS: ( a is sum_of_squares & b is sum_of_squares ) ; :: thesis: a + b is sum_of_squares
then consider f being FinSequence of R such that
A: ( Sum f = a & ( for i being Nat st i in dom f holds
ex a being Element of R st f . i = a ^2 ) ) ;
consider g being FinSequence of R such that
B: ( Sum g = b & ( for i being Nat st i in dom g holds
ex a being Element of R st g . i = a ^2 ) ) by AS;
set t = f ^ g;
C: Sum (f ^ g) = a + b by A, B, RLVECT_1:41;
now :: thesis: for i being Nat st i in dom (f ^ g) holds
ex x being Element of R st (f ^ g) . i = x ^2
let i be Nat; :: thesis: ( i in dom (f ^ g) implies ex x being Element of R st (f ^ g) . x = b2 ^2 )
assume D: i in dom (f ^ g) ; :: thesis: ex x being Element of R st (f ^ g) . x = b2 ^2
per cases ( i in dom f or ex n being Nat st
( n in dom g & i = (len f) + n ) ) by D, FINSEQ_1:25;
suppose E: i in dom f ; :: thesis: ex x being Element of R st (f ^ g) . x = b2 ^2
then (f ^ g) . i = f . i by FINSEQ_1:def 7;
hence ex x being Element of R st (f ^ g) . i = x ^2 by E, A; :: thesis: verum
end;
suppose ex n being Nat st
( n in dom g & i = (len f) + n ) ; :: thesis: ex x being Element of R st (f ^ g) . x = b2 ^2
then consider n being Nat such that
E: ( n in dom g & i = (len f) + n ) ;
(f ^ g) . i = g . n by E, FINSEQ_1:def 7;
hence ex x being Element of R st (f ^ g) . i = x ^2 by E, B; :: thesis: verum
end;
end;
end;
hence a + b is sum_of_squares by C; :: thesis: verum