let R be non empty doubleLoopStr ; :: thesis: for f being FinSequence of R st f is being_an_Amalgam_of_squares holds
f is being_a_generation_from_squares
let f be FinSequence of R; :: thesis: ( f is being_an_Amalgam_of_squares implies f is being_a_generation_from_squares )
assume A1: f is being_an_Amalgam_of_squares ; :: thesis: f is being_a_generation_from_squares
hence len f <> 0 ; :: according to O_RING_1:def 13 :: thesis: for n being Nat st n <> 0 & n <= len f & not f /. n is being_an_amalgam_of_squares holds
ex i, j being Nat st
( ( f /. n = (f /. i) * (f /. j) or f /. n = (f /. i) + (f /. j) ) & i <> 0 & i < n & j <> 0 & j < n )
let n be Nat; :: thesis: ( n <> 0 & n <= len f & not f /. n is being_an_amalgam_of_squares implies ex i, j being Nat st
( ( f /. n = (f /. i) * (f /. j) or f /. n = (f /. i) + (f /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) )
assume A2: ( n <> 0 & n <= len f ) ; :: thesis: ( f /. n is being_an_amalgam_of_squares or ex i, j being Nat st
( ( f /. n = (f /. i) * (f /. j) or f /. n = (f /. i) + (f /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) )
A3: ( ex i, j being Nat st
( f /. n = (f /. i) * (f /. j) & i <> 0 & i < n & j <> 0 & j < n ) & not f /. n is being_an_amalgam_of_squares implies ex i, j being Nat st
( ( f /. n = (f /. i) * (f /. j) or f /. n = (f /. i) + (f /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) ) ;
( f /. n is being_a_product_of_squares & not f /. n is being_an_amalgam_of_squares implies ex i, j being Nat st
( ( f /. n = (f /. i) * (f /. j) or f /. n = (f /. i) + (f /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) ) by Lm19;
hence ( f /. n is being_an_amalgam_of_squares or ex i, j being Nat st
( ( f /. n = (f /. i) * (f /. j) or f /. n = (f /. i) + (f /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) ) by A1, A2, A3; :: thesis: verum