let R be non empty doubleLoopStr ; :: thesis: for f, g being FinSequence of R st f is being_an_Amalgam_of_squares & g is being_an_Amalgam_of_squares holds
f ^ g is being_an_Amalgam_of_squares
let f, g be FinSequence of R; :: thesis: ( f is being_an_Amalgam_of_squares & g is being_an_Amalgam_of_squares implies f ^ g is being_an_Amalgam_of_squares )
assume that
A1: f is being_an_Amalgam_of_squares and
A2: g is being_an_Amalgam_of_squares ; :: thesis: f ^ g is being_an_Amalgam_of_squares
A3: for n being Nat st n <> 0 & n <= len (f ^ g) & not (f ^ g) /. n is being_a_product_of_squares holds
ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n )

proof

let n be Nat; :: thesis: ( n <> 0 & n <= len (f ^ g) & not (f ^ g) /. n is being_a_product_of_squares implies ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n ) )
assume that
A4: n <> 0 and
A5: n <= len (f ^ g) ; :: thesis: ( (f ^ g) /. n is being_a_product_of_squares or ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n ) )
A6: n <= (len f) + (len g) by A5, FINSEQ_1:22;

A7: now :: thesis: ( len f < n & not (f ^ g) /. n is being_a_product_of_squares implies ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n ) )

assume A8: len f < n ; :: thesis: ( (f ^ g) /. n is being_a_product_of_squares or ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n ) )
then consider m being Nat such that
A9: n = (len f) + m by NAT_1:10;
(len f) + m <= (len f) + (len g) by A5, A9, FINSEQ_1:22;
then A10: m <= len g by XREAL_1:6;
A11: m <> 0 by A8, A9;
A12: m <= len g by A6, A9, XREAL_1:6;

A13: now :: thesis: ( ex k, l being Nat st
( g /. m = (g /. k) * (g /. l) & k <> 0 & k < m & l <> 0 & l < m ) & not (f ^ g) /. n is being_a_product_of_squares implies ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n ) )

given k, l being Nat such that A14: g /. m = (g /. k) * (g /. l) and
A15: k <> 0 and
A16: k < m and
A17: l <> 0 and
A18: l < m ; :: thesis: ( (f ^ g) /. n is being_a_product_of_squares or ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n ) )
A19: ( (len f) + k <> 0 & (len f) + l <> 0 ) by A15, A17;
A20: ( (len f) + k < n & (len f) + l < n ) by A9, A16, A18, XREAL_1:6;
(f ^ g) /. n = (g /. k) * (g /. l) by A9, A11, A10, A14, Lm5
.= ((f ^ g) /. ((len f) + k)) * (g /. l) by A12, A15, A16, Lm5, XXREAL_0:2
.= ((f ^ g) /. ((len f) + k)) * ((f ^ g) /. ((len f) + l)) by A12, A17, A18, Lm5, XXREAL_0:2 ;
hence ( (f ^ g) /. n is being_a_product_of_squares or ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n ) ) by A19, A20; :: thesis: verum

end;

( g /. m is being_a_product_of_squares & not (f ^ g) /. n is being_a_product_of_squares implies ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n ) ) by A9, A11, A10, Lm5;
hence ( (f ^ g) /. n is being_a_product_of_squares or ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n ) ) by A2, A11, A10, A13; :: thesis: verum

end;

now :: thesis: ( n <= len f & not (f ^ g) /. n is being_a_product_of_squares implies ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n ) )

assume A21: n <= len f ; :: thesis: ( (f ^ g) /. n is being_a_product_of_squares or ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n ) )

A22: now :: thesis: ( ex k, l being Nat st
( f /. n = (f /. k) * (f /. l) & k <> 0 & k < n & l <> 0 & l < n ) & not (f ^ g) /. n is being_a_product_of_squares implies ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n ) )

given k, l being Nat such that A23: f /. n = (f /. k) * (f /. l) and
A24: ( k <> 0 & k < n ) and
A25: ( l <> 0 & l < n ) ; :: thesis: ( (f ^ g) /. n is being_a_product_of_squares or ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n ) )
(f ^ g) /. n = (f /. k) * (f /. l) by A4, A21, A23, Lm4
.= ((f ^ g) /. k) * (f /. l) by A21, A24, Lm4, XXREAL_0:2
.= ((f ^ g) /. k) * ((f ^ g) /. l) by A21, A25, Lm4, XXREAL_0:2 ;
hence ( (f ^ g) /. n is being_a_product_of_squares or ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n ) ) by A24, A25; :: thesis: verum

end;

( f /. n is being_a_product_of_squares & not (f ^ g) /. n is being_a_product_of_squares implies ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n ) ) by A4, A21, Lm4;
hence ( (f ^ g) /. n is being_a_product_of_squares or ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n ) ) by A1, A4, A21, A22; :: thesis: verum

end;

hence ( (f ^ g) /. n is being_a_product_of_squares or ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n ) ) by A7; :: thesis: verum

end;

len f <> 0 by A1;
then (len f) + (len g) <> 0 ;
then len (f ^ g) <> 0 by FINSEQ_1:22;
hence f ^ g is being_an_Amalgam_of_squares by A3; :: thesis: verum